OpenAI 的千禧年难题证明遭质疑：数学家称“可能自己都没看懂”，1 万个智能体贡献不到 10%

9 月，OpenAI 抛出过一个足够震撼的说法：内部 AI 系统用了大约 88 小时，完成了一道千禧年大奖难题相关的纳维-斯托克斯方程证明。消息一出，“AI 攻克数学”的标题铺天盖地。一个月后，数学界的审查给出了另一种声音：这份 166 页的证明，可能并没有 OpenAI 自己说的那么清楚。

一分钟速览

• OpenAI 于 9 月 8 日公布 166 页证明，称约 1 万个 AI 智能体并行工作 88 小时完成，随后用 17 小时做 Lean 形式化与验证。
• 数学家 Gonzalo Cao-Labora 指出，OpenAI 可能“自己都没看懂就急着发论文”，其方法与西班牙数学家此前的路线只是表面相似。
• 争议核心：证明使用了外部力项，构造出流体速度有限时间无界增长的情形，但并未解决“无外力时三维解是否始终光滑”这一更受关注的问题。
• 纽约大学数学家 Tristan Buckmaster 质疑成果归属，OpenAI 否认使用其数据。
• OpenAI 研究员 Noam Brown 估计，多智能体协作对这次成功的贡献可能不到 10%。

“形式化验证通过”不等于“问题解决了”

先把技术争议说清楚。纳维-斯托克斯方程描述流体运动，是克雷数学研究所设立的七个千禧年大奖难题之一。OpenAI 的证明用 Lean 形式化语言写成，Lean 能检查每一步逻辑推导是否符合规则——这确实是硬功夫，166 页的证明能通过机器检查，说明它至少在形式上是自洽的。

但“形式化验证通过”与“解决了数学家真正关心的问题”是两件事。OpenAI 的证明利用了方程中的外部力项，构造出流体速度在有限时间内无界增长的情形。问题是，克雷研究所的原始表述允许这种情形，而数学界更关注的，是不施加外部力时，三维纳维-斯托克斯方程的解是否始终保持光滑。换句话说，OpenAI 证明的是一个“允许外力”的版本，而不是那个最核心的开放问题。

这也是为什么多位审读专家向《科学美国人》表示，OpenAI 的证明并没有遵循西班牙数学家 Diego Córdoba 与 Luis Martínez-Zoroa 此前探索的路线。Cao-Labora 的说法更直接：OpenAI 可能在发布时并未完全理解自己的模型究竟干了什么。

一万个智能体，贡献了多少？

OpenAI 公布的数字很漂亮：约 1 万个并行智能体、累计约 270 万条消息、约 1300 亿个输出 Token。但这些数字只说明“跑了多少”，不说明“起了多大作用”。

Noam Brown 自己就泼了冷水：多智能体架构对这次成功的贡献可能不到 10%。原因很现实——用数千个智能体做系统性对照实验成本太高，研究人员很难比较“1 个智能体做多久”与“1 万个智能体强多少”。真正关键的，可能是底层模型本身的能力，以及它能否长时间持续处理任务、并行探索多种解法。

这也解释了为什么“1 万个智能体”听起来像产品卖点，而不是科学结论。智能体数量可以堆，Token 可以烧，但科学贡献需要可复现的对照实验来证明。

归属、可读性与“成果洪水”

另一条争议线是归属。Buckmaster 质疑 OpenAI 的研究可能受益于他与 Anthropic 员工 Levent Alpöge 使用公开模型开展的工作。OpenAI 在 9 月 10 日的说明中否认，称调查后认为 Buckmaster 此前两个月在 Codex 中输入的提示词不可能影响研究。双方各执一词，目前没有定论。

更让数学界不安的是发布方式。10 月初，OpenAI 又公开了约 400 项数学研究结果，集中放在 GitHub 上。数学家普遍表示，仅消化这些内容就需要数年；大量成果缺乏充分解释、整理与学术交流，可能模糊“严谨验证”与“大规模自动生成”的边界。

趋势洞察：AI 做数学，需要新的验收标准

这场争议不是要否定 AI 的数学能力。恰恰相反，能在 88 小时内生成 166 页可被 Lean 检查的证明，本身就是工程上的突破。但它暴露出一个更根本的问题：当 AI 可以批量生产“形式正确的证明”时，数学界该用什么标准来判断它的价值？

至少有三件事需要分开看：证明是否解决了目标问题；证明的思路是否可被人类理解、可被复现；成果的归属与贡献如何界定。形式化验证只能回答第一层的一部分，后两层仍然要靠人。

对 OpenAI 来说，真正的考验不是再发多少页证明，而是能否让数学界在数月、数年内完成独立审查。对整个人工智能行业来说，这也是一个提醒：当“AI 攻克难题”成为公关话术时，最稀缺的反而是耐心验证的人。