研究人员在新发表的论文中指出，AI自动形式化系统存在根本性的局限——即使将数学证明成功转换为Lean形式语言并通过机械验证，也无法保证原始自然语言论证的正确性。Alexander Bastounis等研究者以OpenAI宣称的Navier-Stokes方程吹胀解证明为案例，揭示了形式化Lean证明与原始自然语言证明之…