OpenAI 宣称解出纳维–斯托克斯难题：AI 科学真正稀缺的是证明的来路

先说结论

9月8日，OpenAI 宣布：一个尚未公开的内部模型，在约1万名并行智能体协作下，用88小时给出了三维不可压缩纳维–斯托克斯方程有限时间奇异性的证明，并用 Lean 形式化、机器检查。最值得长期跟踪的信号，不是“AI 已经打败数学家”，而是科学研究的工作单元正在变化：模型负责提出路径，代理群负责并行试错，形式系统负责把论证钉死。门槛由“能不能给出答案”移向“答案是否对应正确的问题、来路能否追溯、能否被独立检查”。

事情是怎么发生的

OpenAI说，团队8月28日开始训练新模型，9月1日听到相关传闻后，才把大量资源投入开放问题。项目动用了约1万名并发代理；找到解法用了88小时，Lean 形式化又用了17小时，公开材料包括166页论文和代码仓库。

这里的“解出”要读准：论文构造的是在光滑外力作用下，三维流体速度于有限时间变得无界的例子，对应克雷题目中的 C、D 选项；它不是所有流体的通用解，也不是已经拿到千禧奖。

争议也随即出现。纽约大学数学家 Tristan Buckmaster 与 Anthropic 的 Levent Alpöge 说明，他们此前也用 Claude、Codex 等工具推进相关受迫流体问题。Buckmaster 表示自己没有看过 OpenAI 的证明，不知道数据是否被使用，也没有直接指控抄袭；但他质疑 OpenAI 得知他们进展后才集中投入，并公开了沟通与署名争议。OpenAI 否认使用特定用户数据，同时承认不能排除去标识化数据曾帮助改进模型。事实未定，来源、时间线和署名却已经成为结果可信度的一部分。

为什么重要

这件事把“AI 做科学”从愿景变成了可观察的流水线。一万个代理同时试不同路线，远比一个模型在对话框里写长答案更接近研究；Lean 又把“看起来合理”变成能否通过内核检查。未来科学代理的竞争点，可能不是单次生成质量，而是问题分解、并行搜索、共享中间结果、形式验证和人类决策能否连成闭环。行业因此会更看重算力与组织能力，也更看重可审计记录：模型看过什么、哪些步骤由人决定，都需要留痕。

站得住与站不住的地方

站得住的是证据形态：OpenAI同时发布论文、Lean 代码和对应题目，仓库标注无 sorry，并提供 Comparator 检查入口。这比“模型说它证明了”高一个证据等级。

站不住的是，机器检查不等于数学界已经接受。形式系统能保证写入的命题和证明相互匹配，却不能替人判断命题是否正好击中问题边界，也不能解决关键路线的来源争议。仓库的审阅状态仍是“self-assessed”，OpenAI也说不打算申领奖金。9月9日能下的判断应是“重大、可检查、待同行审阅的候选结果”，而不是“数学史已经翻页”。

接下来该盯什么

第一，看独立数学家能否在干净环境重建并审阅论文与 Lean 证明；第二，看形式化命题与克雷 C、D 选项是否逐条对应；第三，看相关各方能否给出不含隐私的模型输入、时间线和署名规则。若三关都过，AI 科学的标志就不再是“会不会解题”，而是能否把探索、证明和归属一起做成公共基础设施。若过不了，留下的仍是一个重要教训：AI 最先冲垮的，可能不是数学难题，而是人类原有的研究流程。