OpenAI纳维-斯托克斯证明被指Lean转译出错

时间：2026年10月8日（北京时间10月9日凌晨），《新科学家》刊发剑桥大学团队的核查报道；相关预印本于10月6日提交 arXiv。 地点：英国剑桥大学数学研究所（论文作者所在地）；预印本发布于 arXiv；OpenAI 位于美国旧金山，其证明代码托管在 GitHub。 人物：剑桥大学 Anders Hansen、Fabian Circelli 等三位作者（论文题为 Navier-Stokes lost in translation，arXiv:2610.08144，25页）；OpenAI 发言人就报道作出书面回应；数学家 Valerio Capraro 等人在社交平台转发该结论。 事件详情：OpenAI 于9月8日宣布攻克纳维-斯托克斯方程千禧难题，同时发布两个版本的证明——一份是数学家惯用的自然语言版（166页论文），一份是可在 Lean 中机器验证的形式化版，GitHub 仓库称后者是前者结果的形式化。剑桥团队指出两版并不对应：关键分歧在 Lemma 8.6，自然语言证明要求某个取值低于 m+4，而 Lean 版对应位置只要求低于 m+5，后者在数学上更弱、允许更多取值。团队解释，AI 自动形式化的目标是让代码“编译通过”，一旦某段证明无法编译，模型会寻找绕行写法，哪怕因此偏离自然语言原文。OpenAI 回应《新科学家》称，已知悉自然语言证明与 Lean 代码之间的不一致，且这并不意味着任一证明无效，公司将随着核查推进修正自然语言证明中的错误，并继续对本周公开的722篇数学论文做形式化（其中仅部分附带 Lean 证明，且尚未人工核对）。 背景：纳维-斯托克斯方程的整体光滑存在性是七大千禧年难题之一，悬赏100万美元；OpenAI 此前公布166页手稿与 Lean 形式化证明，克雷数学研究所一度对外表示问题“显然已解决”，但数学界的人工核查始终没有结束。同期 OpenAI 一次性放出722篇数学手稿引发学界抵制，又有3项研究被撤回，AI 数学结论的可信度正处在风口浪尖。 影响：研究团队强调，他们并不是说自然语言证明错了——“我们既不说它错，也不说它对”，而是 OpenAI 把两版证明当作同一件东西来呈现。Hansen 表示，所有大语言模型生成的证明今后都必须由人眼通读，这给数学家带来巨大的额外负担；Circelli 指出，自动形式化试图取代同行评审，但论文表明它做不到同样的事。论文还给出一般性论证：要语义忠实地消解自然语言数学文本的歧义，其可解性复杂度指标为无穷，比停机问题（指标为1）更难，因此“Lean 编译通过”无法自动保证自然语言证明成立。 总结：这是 OpenAI 纳维-斯托克斯证明首次遭遇公开、具体的技术性质疑——错配精确到一条引理的不等式常数。事件把争论从“AI 能不能做数学”推向“AI 证明该如何被验证”：OpenAI 已承认不一致并承诺修订，最终结论仍取决于数学家逐行人工审读与克雷数学研究所的裁定。 参考来源： 1. https://www.newscientist.com/article/2592824-openai-mistranslated-mathematics-into-code-for-its-navier-stokes-proof/ 2. https://arxiv.org/abs/2610.08144 3. http://www.damtp.cam.ac.uk/research/afha/anders/NavierStokes_LostInTranslation_Final.pdf 4. https://news.ycombinator.com/item?id=49994145 5. https://en.wikipedia.org/wiki/Navier%E2%80%93Stokes_priority_controversy 6. https://community.openai.com/t/openai-agents-solve-the-navier-stokes-existence-and-smoothness-problem/1395873 7. https://www.tuftsdaily.com/article/2026/09/mathematicians-still-checking-the-navier-stokes-proof-that-openai-claims-to-have-solved