2026 年 9 月 8 日，OpenAI 公布了一份纳维–斯托克斯方程的奇点证明及 Lean 形式化，称其内部 AI 系统解决了这项千禧年难题。找到结果的小组规模约为一万个并发 Agent，使用的是尚未公开的新内部模型。官方公告
这份成果提出了一个具体的反例：原本静止的三维不可压缩黏性流体，在光滑外力作用下，局部速度可以在有限时间内变得无界，同时总动能始终有界。它把一个长期数学问题推进到可公开审查的证明，也把 AI 科研的三个环节摆在了一起：如何找到结果、如何检查结果，以及如何交代发现过程。
外力保持光滑，流体速度却变得无界
纳维–斯托克斯方程描述流体的速度、压力与黏性如何共同决定运动。难题在于：从足够平滑的状态出发，运动能否一直平滑延续，还是会在某个时刻出现奇点？黏性会抹平速度差异，让“越来越剧烈的运动”与“耗散”之间的竞争格外难以处理。
OpenAI 论文构造的涡旋向内收缩、加速，形状越来越细长；这里半径与轴向尺度都在缩小，只是半径缩得更快。高速运动集中到越来越小的区域，使局部速度无界与整体动能有界能够同时成立。
关键一步发生在涡旋与外部流动衔接的位置。论文加入振荡扰动，让流体自身输运动量，抵消原先会发散的不平衡项；最后留下的外力及其各阶导数，仍能平滑穿过奇异时刻。构造的要害就是让异常来自流体运动，而外力满足题目要求。论文，第 1、3—6 页
“有外力”符合 Clay 的正式题目。题面列出 A、B、C、D 四个版本，证明其中之一即可：A、B 要求在无外力条件下，任意符合条件的初态都有满足题目要求的全局光滑解；C、D 允许光滑外力，寻找这类全局解无法存在的情形，其中 C 所要求的解还须满足动能一致有界的条件。OpenAI 对应的是 C、D，分别涉及整个三维空间和周期空间。这个范围既足以对应官方挑战，也应与无外力的纳维–斯托克斯问题区分。Clay 官方题目
研究路线已有积累，Agent 扩大了探索规模
在这次公告之前，研究者已经沿着“逐层加入扰动、控制外力”的方向推进。陶哲轩在 9 月 7 日的分析中，把基本思路归于 Diego Córdoba 与 Luis Martínez-Zoroa：利用背景流动的不稳定性，让最初很小的高频修正逐渐放大，同时约束它给外力带来的变化。Alpöge 与 Buckmaster 将相关方法推进到有光滑外力的 Euler 等方程。
这说明此次事件有明确的数学来路。AI 研究的增量，需要放在既有构造方法与尚未跨过的技术障碍之间衡量。陶哲轩的机制分析
OpenAI 披露的组织方式，也包含连续的研究决策：不同 Agent 小组探索不同题目版本，获得自家 Euler 结果后，团队把更多资源转向纳维–斯托克斯，并用 Codex 汇总各组有用的中间发现，再反馈给后续探索。Agent 可以读缓存网页、运行代码；过程中还更换了继续训练后的模型。官方研究过程
据 Quanta 对这次工作的报道，寻找纳维–斯托克斯证明耗时约 88 小时，后续形式化另用约 17 小时。Quanta 报道
这段时间背后的计算量很大：OpenAI 披露，纳维–斯托克斯项目消耗约 1300 亿个输出 token。88 小时衡量的是并行探索经过的时间；评价科研效率，还要看多少计算投入换来有效发现，以及结果能否被其他研究者复用。官方用量披露
Lean 提供检查入口，数学理解仍需继续
OpenAI 同步公开的仓库包含 Navier–Stokes 与 Euler 的 Lean 4 形式化、构建步骤和独立检查入口。外部研究者因此拿到了可以进一步检查的证明文件。公开仓库
发布者的元数据声明，主结果已完整形式化，没有用 sorry 留下待证明的空缺；同一文件把审查状态标为 self-assessed，即自评。这些字段说明作者声称完成了什么，尚不构成第三方复跑记录。形式化元数据
Lean 检查形式系统内的推导，研究者还要确认形式化命题忠实表达了原始数学问题，并理解构造为何有效。Quanta 在报道中明确保留了进一步审查的条件，也指出这种命题对应关系需要人类核对。Quanta 对验证边界的说明
奖金认定另有程序。Clay 的规则要求成果在合格渠道发表、至少经过两年，并获得全球数学界的普遍接受，才会进入考虑范围。因此，证明公开、形式检查与获奖认定各有自己的证据要求。Clay 奖金规则
同期成果把发现过程也推到了台前
Buckmaster 在同期公开声明中说，他与 Levent Alpöge 使用多家公司的模型推进研究，在 8 月 22 日完成相关 Euler 证明的 Lean 验证，之后一直尝试把模型产出的论证改写得更易读。他强调这是两人的个人合作，并将基本研究路线归功于 Córdoba 与 Martínez-Zoroa。
声明也提出了发表协调、署名安排和研究数据使用方面的疑问。Buckmaster 同时明确表示，自己尚未看到 OpenAI 的证明，也不知道对方是否使用了他们的数据。Buckmaster 声明
OpenAI 承认对方在有外力 Euler 研究上的优先权，否认研究者或 Agent 在成果公开前看到过对方工作，也否认针对解题访问特定用户数据；公司同时表示，无法完全排除去标识化的产品使用数据曾帮助改进模型。OpenAI 回应
公开材料不足以据此裁定数据是否被使用。它们已经说明，证明能否成立与发现过程能否交代清楚，是科研团队必须分别回答的问题。
对建设科研 Agent 的团队，这次事件给出了一项具体要求：在扩大并行探索时，保存人类指导、输入材料和中间结果的来源，并让最终论证能够被外部研究者检查。接下来最有价值的进展，是同行能否把这份庞大的证明提炼为可理解、可复用的方法，再用它推进新的数学问题。那将决定一次集中计算获得的成果，能够为后续研究节省多少工作。
