剑桥大学数学家安德斯·汉森（Anders Hansen）及其团队指出，OpenAI 在公布纳维埃-斯托克斯方程证明时存在一个微妙但关键的问题：其发布的自然语言版本与用于计算机验证的 Lean 代码版本并不匹配。这一发现并未直接否定 OpenAI 解决了该数学难题，但引发了对大型语言模型生成数学结果可靠性的质疑。
汉森表示：“所有由大型语言模型生成的证明都必须经过人类阅读，这给数学家带来了巨大的额外负担。”
9 月 8 日，OpenAI 宣布找到了纳维埃-斯托克斯问题的解决方案，并发布了两个版本的证明：一个是结合英语和数学符号的自然语言版本，另一个是 Lean 4 形式的“精简证明”。后者通过形式化过程允许计算机机械地验证逻辑陈述的真实性。然而，汉森团队认为这两个版本在逻辑上存在差异。
团队成员、同样来自剑桥大学的 Fabian Circelli 解释道：“同行评审意味着人类肉眼检查证据。但我们在这篇论文中展示的是，使用这种类型的人工智能进行自动形式化并不能达到同样的目的。”
Read more在 OpenAI 的 722 篇新论文中最有趣的数学发现
研究人员强调，他们并非断言 OpenAI 未能解决纳维埃-斯托克斯问题。正如毕达哥拉斯定理有数百个有效证明一样，自然语言证明和 Lean 证明可能各自提供有效的解决方案。核心争议在于 OpenAI 将这两种形式呈现为完全一致的结果。
汉森指出：“我们不是说自然语言证明是错误的，也不说它是正确的。问题在于 OpenAI 声称其 GitHub 库中的 Lean 4 结果是论文中所述内容的形式化版本，但实际上两者存在‘翻译错误’。”
这种不匹配源于 AI 必须生成能够“编译”的 Lean 证明，即代码需完全自洽且不报错。如果在自动形式化过程中发现某些部分无法编译，AI 可能会试图寻找替代方案，即使这意味着偏离原始自然语言证明的逻辑。
Read moreOpenAI 已经丢弃了 722 篇数学论文，现在它必须清理一下。
具体差异出现在证明的第 8.6 引理（Lemma 8.6）部分。在自然语言证明中，相关方程要求一定值低于 m+4（m 为整数）；而在 Lean 证明中，等价值必须低于 m+5。从数学角度看，后者是一个更弱的条件。
汉森举例说明：“想象解出 x+3=6，答案是 x=3。我们可以写出证明 x 小于 4，也可以写 x 小于 5。两者都是正确的数学命题，但它们表述不同。后一个证明允许 x 有更多可能的取值，因此在数学上更弱。”
OpenAI 向《新科学家》回应称，已意识到自然语言证明与 Lean 代码之间的不匹配，但这并不意味着任何证明无效。公司将继续对其本周发布的 722 篇数学论文进行形式化处理，目前仅部分论文附带了精简证明。
检验堆中的针
识别这些差异的过程颇为艰难。研究团队首先利用 ChatGPT 寻找自然语言和 Lean 证明间的潜在差异，随后进行人工核查。许多由 AI 提出的差异最终被证实是一致的，但真正的差异仍需大量手动工作才能确认。汉森形容这一过程为“一场噩梦”，团队耗时约两周才确定真正的差异点。
伦敦国王学院的团队成员 Alexander Bastounis 评论道：“OpenAI 吹嘘能够快速产生这一结果，但这只是整个验证过程的一部分。”
若数学家要信任此类结果，必须回答 AI 模型能否准确地进行自动形式化。汉森团队证明，ChatGPT 可以生成与原始自然语言不匹配的 Lean 版本，并在过程中默默改变逻辑论证以掩盖错误。“它试图帮助我，但这样做并没有帮助，”汉森说。
对于漫长而复杂的证明，除非仔细对比两个版本的细节，否则很难注意到这种细微差别。鉴于 OpenAI 刚刚发布了 722 篇论文，这一问题变得尤为紧迫。汉森警告：“如果我们认为‘所有这些现在都是真的，我们唯一需要做的就是阅读报纸’，那是非常危险的。科学的目的是让人类了解世界运作机制以便做出明智决定。如果我们失去这种理解，我们在做什么？”
伦敦帝国理工学院的 Kevin Buzzard 指出，在此类讨论中区分定理陈述与证明至关重要。例如，费马最后定理的陈述易于转换为 Lean 并检查。一旦确认 Lean 中的陈述正确且证明能编译，即可相信证明为真。
Buzzard 补充道：“问题在于，正如汉森团队所指出的，这对以 PDF 文件形式发布的自然语言版本一无所知。我相信纳维埃-斯托克斯问题得到了正确解决，但我不太相信 PDF 中描述的证明是正确的。”
汉森希望 OpenAI 认真对待该团队的工作，并在开发强大的自动形式化技术上投入更多精力。他总结道：“我们有解决方案吗？还没有。能否以一种可控的方式做到这一点？是的，但它将是怎样的，最优和最终的方法目前尚不清楚。”
Journal reference:arXiv DOI: 10.48550/arXiv.2610.08144
