在一篇新论文指出 OpenAI 早先公布的 Navier–Stokes 证明 与其经计算机校验的版本对不上后，数学界开始质疑：OpenAI 这 719 篇由 AI 生成的数学论文，到底能信到什么程度？
要点概览：
- OpenAI 起初发布 722 篇 AI 数学稿件，因发现符号号记错误撤下 3 篇，目前目录减至 719 篇。
- 英国三位数学家发现，Navier–Stokes 书面证明与对应的 Lean 代码在两个关键位置出现分歧。
- 论文作者并未直接断言证明错误，但强调：机器形式化校验无法替代传统同行评审。
OpenAI 的数学论文发布
OpenAI 于 10 月 6 日在网上集中发布这批 AI 数学稿件。周四公布的一份报告 指出， OpenAI 的做法偏离了一支独立数学家小组给 AI 实验室制定的操作指引。该目录最初收录 722 篇稿件， 但 OpenAI 在次日就通过 公告 撤回了其中 3 篇：一篇因符号正负号使用错误导致论证崩塌，另外两篇则依赖于该结论，只能一并下架。
这份由九人组成的“数学与人工智能咨询小组”在 9 月 29 日 发布 的指引开宗明义，呼吁各家实验室停止在闭源大模型上测试高难度数学难题。 而 OpenAI 的代码库则说明，这批论文源自公司对一个尚未公开的内部模型，在开放数学研究问题上的系统性评估。
目前，仅有 10 个结果附带了模型推理过程的自然语言概要；约 42% 的“主结果”被形式化到了 Lean 中—— Lean 是一种可由计算机逐步核查证明正确性的形式化证明语言。
延伸阅读：Anthropic CEO 年薪几何？IPO 招股书给出答案
Navier–Stokes 证明的“错位”
伦敦国王学院的 Alexander Bastounis，以及剑桥大学的 Fabian Circelli 和 Anders Hansen， 对 OpenAI 在 9 月宣布攻克的 Navier–Stokes 证明进行了 审查。三人记录了书面证明与 Lean 代码出现分歧的两个具体位置， 其中一处涉及估计强度：Lean 代码给出的只是一个明显更弱的估计，而论文正文却声称获得了更强的结论。
论文作者刻意避免就书面证明“真伪”下最终定论，他们的论点更为收敛： Lean 的形式化证明确实验证了最终定理成立，但无法检查人类可读版本中每一步中间推理是否严谨。 换言之，即便有机器校验背书，这类成果仍离不开传统意义上的同行评议与细致人工审读。
菲尔兹奖得主 陶哲轩（Terence Tao） 在 10 月 6 日 发文 指出， 目前许多难题正由“AI 提示工程师”推动解决，而这些人往往并未真正理解模型吐出的证明， 以致无法就相关工作回答深入问题，甚至难以就此做一场像样的学术报告。 顾问小组成员、哈佛大学教授 Melanie Matchett Wood 则表示， 此类成果发布时，“实际上没有任何一个人真正理解它们”， 真正的工作反而是从发布那一刻才刚刚开始。
围绕 OpenAI 证明的争议
顾问小组此前强调，只有更广泛的数学界，才能评判 OpenAI 在多大程度上遵守了相关建议。 如今的审视，叠加的是一个本就紧张的月份：OpenAI 在 9 月 8 日宣布 Navier–Stokes 结果， 立即与纽约大学数学家 Tristan Buckmaster 发生署名与优先权纠纷。 三天后，25 位菲尔兹奖得主联署声明，警告大规模“批量生产”式的 AI 数学结果可能对学科生态造成伤害。
