FRONTIER · 落到现实

一万个 agent 跑了 88 小时，纳维-斯托克斯方程被证明会「炸」——Lean 说证明是对的，功劳却还没算清

Finite Time Blowup for Navier–Stokes / On the Navier–Stokes Millennium Prize Problem

OpenAI 以公司名义署名、不列个人作者的 165 页预印本 · 由一个仍在训练、官方称明显强于 GPT-6 Astra 的内部模型驱动约一万个并发 agent 产出 · 附 Lean 4 形式化证明，任何人都可以用 Comparator 独立复核

2026 年 9 月

为什么选它千禧年难题第一次被认真宣称由 AI 拿下，而且附了机器可核的证明。但这篇入选不只因为结果：它把「证了什么、怎么找到的、功劳归谁」三件事同时摆上了桌面。我们对照了 OpenAI 原文、另一组数学家的声明和陶哲轩的博客，把三件事拆开讲清楚。

9 月 8 日，OpenAI 挂出一篇 165 页的预印本，标题只有一行：《纳维-斯托克斯方程的有限时间爆破》。署名不是任何个人，就是「OpenAI」。它宣称解决了克雷数学研究所 2000 年列出的七个千禧年大奖难题之一，证明由一个尚未发布的内部模型驱动的多智能体系统产出，另附一份 Lean 形式化证明。这是千禧年难题第一次被认真地宣称由 AI 拿下，而且它的正确性不靠任何人的名声担保，而是交给机器去核。

但这篇值得读，不只是因为结果本身。围绕它有三个问题——它到底证了什么、机器是怎么找到它的、功劳该怎么算——每一个都比「AI 解出了千禧年难题」这个标题更值得弄清楚。本文以 OpenAI 的论文和代码仓库为主，同时对照了同一条路线上另一组数学家 Buckmaster 的公开声明和陶哲轩的博客：这件事只听一方讲，一定会讲歪。

它到底证了什么

纳维-斯托克斯方程用牛顿第二定律描述不可压缩流体怎么动，天气预报、飞机设计、血流模拟都靠它。方程里有一个粘性项，可以理解为流体内部的摩擦，它总想把速度的尖峰抹平。九十年来悬而未决的问题是：从光滑的状态出发，三维流体会不会在有限时间内、在某一点上速度冲到无穷大？这叫「爆破」（blowup），也就是出现奇点。1934 年 Leray 证明了广义意义上的解一直存在，但它会不会始终光滑，没人知道。

克雷的官方题面（由 Fefferman 撰写）列了四个选项，证出任意一个都算解决：A、B 是「永远光滑」，C、D 是「会坏掉」，而且 C、D 允许对流体施加外力，只要外力本身光滑。OpenAI 证的正是 C（全空间）和 D（周期箱体）：对任意正的粘性，都能造出一个从静止出发、只受一个在时间和空间上都局限在有限范围内的光滑外力、总动能始终有界，速度却在有限时刻冲向无穷的解。

构造的核心是一根越转越细的涡旋，像被越拉越长的意大利面：半径缩得比高度快，转速不断上升，总动能反而趋于零。难点在于，光靠这根涡旋，维持它所需的外力本身会发散，不合规则。论文的办法是在涡旋外围的环带里加一串振荡的「脉冲」，让流体自身的非线性动量输运去抵消那部分发散，剩下的外力才能光滑地穿过奇点时刻。论文把 Córdoba 与 Martínez-Zoroa 的工作列为最直接的前驱：同样是跨尺度逐级放大，只是被放大的扰动在这里扮演了新角色。

有一点需要知道：带外力这条路不是冷门，但也不是最硬的那条。陶哲轩在 OpenAI 公布前一天的博客里写道，学界普遍预期能构造出光滑外力下的爆破，甚至不加外力也行。按克雷的规则，C 是完全合法的答案；但在很多人心里，无外力版本才是物理上最想知道的那个。

一万个 agent 是怎么排兵布阵的

OpenAI 在同步发布的博客里交代了过程。8 月 28 日开始训练的一个新内部模型，数学能力出现跳变，官方说法是明显强于 GPT-6 Astra，而且还在继续训练。9 月 1 日他们听到传闻说有两道千禧年难题被解决，于是把模型拉去打所有未解的千禧年问题，外加一批「简单一点」的问题。agent 分成若干组，组内可以互相通信，能读一份缓存版互联网，能跑代码；证明「光滑」和证明「会坏」的题面分给不同的组。

意外先出在副线上：把粘性去掉的欧拉方程，将近 100 个 agent 跑了约 50 小时，做出了无外力的爆破。看到这个结果，团队把其他千禧年问题上的 agent 全部调到纳维-斯托克斯，把欧拉的解喂给它们；中途模型训练出了新版本，就直接换上；还定期用 Codex 把各组最有用的中间发现汇总，再回灌给各组——最终找到答案的那组就是这样被引导的。9 月 5 日，距首批 agent 启动约 88 小时，结果出来了；又花 17 小时，由 GPT-6 Astra 完成 Lean 形式化。光这一题，同时在线约一万个 agent，发了 270 万条消息，用了约 1300 亿输出 token。

标题最容易吞掉的是：这不是「把题目丢给模型，它自己解了」。选题、分组、换模型、把副线成果转成主线提示、用另一个模型做跨组的知识整合，每一步都是人做的调度决策。这和第 23 篇「16 个 Claude 写编译器」是同一种结构：真正的产品是编排，而不只是单个模型。

Lean 把「对不对」交给了机器，也把问题挪了个地方

Lean 是一种证明助手：把数学命题和证明写成程序，编译通过就意味着每一步推导都被机器逐条检查过。OpenAI 的仓库还配了 Comparator 挑战，让任何人都能在隔离环境里核对两件事：证明能编译，且它证的正是那条事先约定好的命题。这条命题的写法，改编自 Google DeepMind 的 Formal Conjectures 项目——一份外人早就写好的千禧年题面形式化。

这很关键。第 57 篇讲过，AI 把费马大定理写成 Lean 之后，被自动化掉的是审稿。这里同理：只要你相信 Lean 的内核，并且相信那份形式化题面忠实于克雷原文，一百多页的正确性就不再需要一群专家熬几个月。信任被压缩到了一页纸上：那条命题写得对不对。这比「请相信我们的专家」强太多。

但它没回答的问题也很清楚：这个构造为什么行得通，人类从中学到了什么。陶哲轩在博客里说得很直白，解题只是代理目标，真正的目标是理解。Buckmaster 则形容自己那份 AI 起草的欧拉稿子「只能叫 AI slop」，正在拼命改写成人读得懂的样子。第 24 篇里陶哲轩预言的「证明过剩」，现在来了：证明是对的，消化还没开始。

功劳怎么算

另一条线上，纽约大学的 Buckmaster 与在 Anthropic 任职的数学家 Alpöge，以个人合作的形式沿 Córdoba 与 Martínez-Zoroa 的光滑外力路线推进了将近一年，其间用过 Claude 和 OpenAI 的 Codex 等多个模型。8 月 15 日他们拿到欧拉与 Boussinesq 方程的光滑外力爆破，一周后 Lean 验证通过，9 月 7 日公开。

双方的叙述有明显出入。OpenAI 说，他们是 9 月 1 日听到传闻才起跑的，此前没有通过任何途径看过对方的工作；内部调查确认 Buckmaster 过去两个月在 Codex 里的提示不可能影响到这个系统；承认对方在带外力欧拉问题上的优先权，并表示不申领克雷奖金。Buckmaster 的声明则说，他们的全部草稿都放在 Codex 里；外力这条路几乎没人在走，不是给模型一个题面几天就能摸到的方向；他起初被告知「几乎没有人类介入」，谈下去才知道背后有整支团队、多轮调度和海量算力。他同时写明：自己没看过 OpenAI 的证明，不指控任何人，只陈述被告知了什么。

谁对谁错，我们不下判断。值得记住的是它暴露的结构问题：当同一家公司既卖给你研究工具，又自己下场做同一道题，一则传闻本身就成了信号。Buckmaster 事后对《卫报》说，现在数学界最大的新闻是，没有人愿意分享任何东西了。

这件事最该带走的数字不是「一万」，而是两条时间线的落差。按 Buckmaster 的自述，他们花了大半年缓慢推进，外力欧拉从突破到 Lean 通过用了一周；OpenAI 从起跑到纳维-斯托克斯定稿，不到四天。一旦某个问题被公认「可以攻了」，谁的算力铺得开谁先到——这是第 1 篇苦涩的教训在纯数学里的版本：方法上没有新招，赢在把搜索铺成一万路并行。第 48 篇说 AI 的加速是斑块状的，现在又多了一块斑，而且是最硬的那块。其次，Lean 改变了这类争议的性质。佩雷尔曼的庞加莱猜想证明，数学界花了三四年才核完；现在「对不对」可以在几天内由任何人独立复核，争议立刻转移到「是谁的」和「意味着什么」——恰好是机器判不了的两件事。那些信奉「开放分享才能快」的领域，这下要面对一个真实的博弈：把草稿放在谁的工具里，本身成了风险。最后，别忽略 OpenAI 自己写下的动机：让世界知道 AI 进展有多快。这次用的是一个还在训练、尚未发布的内部模型，所以它首先是一次能力展示，也是第 40 篇所说「研究自动化」临界点的一个公开数据点。同一篇博客末尾说，要对进展的节奏做更审慎的选择。把它和第 33 篇那 1,367 人要一个刹车装置对照着读，味道很复杂：最有能力踩刹车的人，正在用最快的速度证明这辆车有多快。

AI for Math纳维-斯托克斯多智能体Lean 形式化科研归属

去读原文 本文是原创导读，不是原文翻译——真正的细节、证据和微妙之处都在原文里。原文OpenAI · Finite Time Blowup for Navier–Stokes（预印本全文）→ 代码Lean 4 形式化证明与 Comparator 复核说明（仓库内附官方博客链接）→ 延伸Tristan Buckmaster 的公开声明：另一条线上的时间线与分歧 → 延伸陶哲轩博客：光滑外力爆破这条路线的思路 → 延伸The Guardian：数学家们怎么看 →

上一篇两个不会写 kernel 的生物学家盯着 Claude 干了四周：30 多个开源生物模型平均快 4 倍，一万美元一个靶点的设计跑成了一百五下一篇把 agent 走过的弯路原样存下来，就是一个不用训练的模拟器——几千套搜索策略在「梦里」试完，真正上机的调用少了四成

本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。篇目由编辑独立选取，来源均经人工核实。