在一篇最新论文提出 OpenAI 早前公布的 Navier–Stokes 证明与其计算机核查版本不相符之后，数学界开始审视，这家机构以 AI 生成的 719 篇数学稿件究竟能否信赖。
要点概览：
- OpenAI 最初释出的 AI 数学稿件从 722 篇缩减至 719 篇，原因是公司因符号号记错误撤下 3 篇论文。
- 三名英国数学家记录到，OpenAI 的 Navier–Stokes 书面证明与 Lean 代码在两个关键环节出现分歧。
- 论文作者并未直接断言该证明错误，但强调机器校验无法取代传统的同行评审。
OpenAI 数学成果发布
OpenAI 于 10 月 6 日集中公布这批数学成果。随后在周四发布的一份报告中，研究者指出，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 数学结果可能损害整个学科生态。
