专题 · FULL STORY

OpenAI数学证明风波：质疑、撤稿与验证

剑桥团队发表论文质疑Lean验证可信度，直指OpenAI的Navier-Stokes证明；OpenAI随即公开math仓库并撤回3篇霍奇猜想手稿；随后有研究者基于其成果做出改进并用Lean形式化验证，风波持续发酵。

2026-10-08 ~ 2026-10-09 · 3 集 · 21 条

第 1 集 · 剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(2026-10-08,14 条)

剑桥学者 Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen 在 arXiv 发表论文《Navier-Stokes lost in translation》（编号 2610.08144），系统质疑「AI 自动形式化 + Lean 机械验证」背书数学证明的做法，并直指 OpenAI 此前宣布的 Navier-Stokes 方程解 blow-up 证明疑点。论文从理论与实例两方面表明 Lean 校验通过并不能回溯保证原始自然语言证明正确，值得所有关注 AI 数学证明可信度的人重视。

已确认

  • 论文核心论点：将自然语言证明自动形式化（autoformalisation）为 Lean 并通过 Lean 校验，不能说明原始自然语言证明是正确的。
  • 作者展示了具体案例：聊天模型把一个错误的证明「悄悄修正」后翻译成合法的 Lean 证明，Lean 校验照样通过，即翻译过程可能掩盖原证明的错误。
  • 论文从理论上证明忠实翻译问题本身不可判定，相关的自然语言歧义翻译难度高于停机问题。
  • 论文明确以 OpenAI 宣称的 Navier-Stokes 证明为质疑对象，指出其 Lean 形式化版本与原论文的证明路线并不一致，形式化智能体有时会走与被形式化的非正式证明不同的路线，依赖的验证流程存在根本缺陷。
  • Pedro Domingos、Rohit Paul、Anshul Kundaje、Rex Douglass 等多位博主转发该论文并强调其影响。
  • Valerio Capraro 也独立指出 OpenAI 声称的 Navier–Stokes 解答与其 Lean 形式化验证不匹配，并推荐该论文，称形式化过程可能「偷换定理」，即通过 Lean 验证既不自动保证自然语言证明正确，也不意味着形式化陈述真正捕捉了原定理。

尚未确认

  • 围绕「GPT-6 是否修复了 Peter Bel 的错误 Navier-Stokes 证明」的讨论，Elliot Glazer 持保留意见：他倾向于认为 Lean 形式化证明与英文论文并非一一对应，GPT 的形式化被指对难证引理抄近路，这进一步削弱了「去形式化（deformalization）」的可信度，但这属于个人判断而非论文结论。

为什么重要

  • 若 Lean 验证通过不能回溯保证原证明正确，AI 数学证明宣称的可信度需要重新评估，形式化验证在 AI 数学工作流中的角色面临根本性挑战。

第 2 集 · OpenAI 数学仓库因符号错误撤回 3 篇霍奇猜想论文(2026-10-08,5 条)

OpenAI 在公开 openai/math 仓库仅两天后发布首份更新日志：撤回 3 篇手稿、修订 14 篇、更新 13 篇引用，手稿总数从 722 降至 719。撤稿原因是一处符号错误使一个稳定性-迹相消（stability-trace cancellation）论证失效，另两篇依赖该论证的论文随之撤回；据机器之心转述，三篇均与霍奇猜想相关，涉及 Weil 类代数性与 K3 曲面等内容。

已确认

  • OpenAI 于 10 月 7 日前后撤回 3 篇论文，并修订其余 14 份手稿。
  • 仓库新增 6 个 Lean 形式化、19 处修改。
  • 在 719 项核心（顶线）结果中，约 300 项、即约 42% 已完成 Lean 形式化，团队表示将持续更新。

为什么重要

  • 事件显示形式化验证正在成为 AI 生成数学成果的可信度把关机制：错误由 Lean 形式化流程暴露并促成及时撤稿。
  • 42% 的形式化覆盖率意味着多数结果尚未经机器验证，该仓库的可信度仍有待后续形式化工作逐步确认。

第 3 集 · 研究者用 Lean 验证并改进 OpenAI 数学证明(2026-10-08,2 条)

有研究者声称在 OpenAI 近期数学证明成果的基础上做出了显著改进，并通过 Lean 形式化证明系统对改进进行了验证。相关代码已在 GitHub（CrocSwap/integer-mult-bounds）上开源，供社区查阅和核查。