OpenAI在9月8日宣布解决了纳维-斯托克斯问题，这是数学界最著名的未解难题之一。它同时发布了两份证明：一份用自然语言写成，也就是人类数学家习惯的英语加数学符号；另一份用Lean代码写成，供计算机机械验证每一条逻辑陈述是否为真。

剑桥大学的Anders Hansen和他的团队发现，这两份证明对不上。

打开网易新闻 查看精彩图片

这不是说OpenAI没解出纳维-斯托克斯问题。两份证明完全可能各自都成立，就像勾股定理有几百种正确证法。问题更微妙：OpenAI的模型在把自然语言转成Lean代码时，翻译错了。

错在哪一行

分歧点落在证明中一个叫Lemma 8.6的部分。自然语言版本里，这个部分的某个方程要求一个值小于m+4，m是整数。到了Lean版本里，对应的值变成了小于m+5，这在数学上更弱。

打个比方：解方程x+3=6，答案是x=3。你可以证明x小于4，也可以证明x小于5，两个陈述都对，但说的不是一回事。后一个证明允许x有更多可能取值，数学上就更弱。

Hansen说：“我们不是说自然语言证明是错的，也没说它是对的。”问题在于OpenAI把两份证明当作等同物呈现，在Github上写道：“这个仓库包含论文《纳维-斯托克斯的有限时间爆破》中结果的Lean 4形式化。”

为什么会翻译错？Hansen解释，AI必须产出一份能“编译”的Lean证明，也就是代码完全自洽、不报错。如果在自动形式化过程中遇到某段证明编译不过，AI会想办法绕过去，哪怕这意味着偏离自然语言写成的原证明。

两周对88小时

找出这个分歧的过程有点超现实：团队先让ChatGPT去找自然语言证明和Lean证明之间可能的差异，再逐条手工核对。ChatGPT给出的很多差异，人工检查后发现其实是一致的。

Hansen说：“手工过一遍这些东西简直是噩梦。”整个团队花了大约两周才确认一处真正的分歧。相比之下，OpenAI说它的智能体生成这些证明花了88小时。

伦敦国王学院的团队成员Alexander Bastounis说：“OpenAI炫耀他们能多快生成这个结果，但那只是整个过程的一部分。”

剑桥大学的Fabian Circelli说：“这个形式化过程试图取代同行评审。同行评审意味着人眼去看证明。但我们在这篇论文里展示的是，用这类AI自动形式化无法起到同样的作用。”

722篇论文的隐忧

OpenAI对New Scientist表示，它知道自然语言证明和Lean代码之间存在不匹配，但这不意味着任何一份证明无效。它说会修正自然语言证明中发现的任何错误，也会继续形式化本周发布的722篇数学论文——其中只有一部分附带了Lean证明，而这些Lean证明本身也没有经过人工检查。

如果这种情况发生在一份又长又复杂的证明里，不仔细检查两个版本，很难有人注意到。这个问题因为那722篇论文的发布而更加紧迫。

Hansen说：“如果我们觉得‘这些现在都是真的了，我们只需要读论文就行’，那是危险的。做科学的目的，是人类应该理解世界如何运作，从而做出有根据的决策。如果我们失去了这种理解，我们在做什么？”

帝国理工学院的Kevin Buzzard指出，这类讨论中要区分定理的陈述和它的证明。比如费马大定理的陈述是：对于正整数a、b、c和n，aⁿ+bⁿ=cⁿ只在n为1或2时成立。这个陈述很容易转成Lean并检查。一旦你确认Lean里的陈述正确，且该陈述的证明能编译通过，你就可以确信证明为真。

Hansen团队的核心担忧在于：ChatGPT确实可能产出一份Lean证明，它和原始自然语言证明不匹配，AI在过程中悄悄改动了逻辑论证来掩盖错误。Hansen说：“它想帮我，但这么做，反而没帮上。”

Hansen说：“所有这些大语言模型生成的证明，都必须由人类来读，这给数学家带来了巨大的额外负担。”