水会炸：OpenAI 十万个 Agent、88 小时、167 页证明，推倒了 Navier-Stokes 的半边天

9 月 8 日夜里，Hacker News 首页同时挂着两个爆炸帖。一个指向 NYU 数学教授 Tristan Buckmaster 的一纸声明，一千二百多分；另一个指向 OpenAI 官博《On the Navier–Stokes Millennium Prize Problem》，一千零八十八分，九百多楼评论吵成了一锅粥。千禧年七大数学难题里最出名的那一个，一夜之间被两拨人同时宣布动过——一拨是人类数学家，另一拨，是十万台 AI。

先说结论里最反直觉的一句：没有任何一方宣称证明了「水不爆炸」。两支团队攻的都是这座堡垒的另一面。

千禧年难题的细纹

2000 年，克雷数学研究所把 Navier-Stokes 方程的解的存在性与光滑性挂上一百万美元。官方文件其实开了两扇门。一扇是正门：(A)(B) 两条，要求证明三维不可压 Navier-Stokes 方程对光滑初始数据永远光滑，外力必须为零。另一扇是侧门：(C)(D) 两条，只要你能找到一个反例——光滑的数据，配上光滑的外力，让解在有限时间内失去光滑性，同样算解决问题。

细纹就在侧门的措辞里：外力允许你自己设计。这话的分量，相当于允许你自己画考卷上的辅助线。绝大多数头条把它略过了，而 OpenAI 打的恰恰是这扇侧门。

OpenAI 那份证明说了什么

按官博和随论文放出的说法：对每一个正的粘性系数，都存在一个光滑外力，使方程从静止出发的解在有限时间内速度无界——而全程动能有界。C 条的三维空间和 D 条的三维环面，两个场地都拿下了。

物理图像相当具体：一股向内螺旋的涡旋，被反复拉伸成越来越细的「意大利面」，模型把高频修正一次次推进线性化算子的不稳定方向，最后整个系统塌缩成一个不稳定的调制 ODE——流体在有限时间里，自己把自己甩了出去。

167 页论文，署名栏只有一个词：OpenAI。同一个仓库里还躺着一份 58 页的结果，证明无外力的三维 Euler 方程从光滑紧支撑数据出发也会有限时间爆破——数学上更干净的头条，反而被发布会埋在了第二段。两个结果全部用 Lean 4 加 Mathlib 形式化完毕，仓库 NavierStokesAndEuler 9 月 8 日上线，几小时八百多星，还自带一个叫 Comparator 的独立复核器。任何人 clone 下来敲一行 lean，就能看着编译器逐条核对这个世纪级结论。

88 小时的账单

过程数字是这次发布里最超现实的部分。内部模型，官方描述为「显著强于 GPT-6 Astra」；约一万条 Agent 并发；9 月 5 日启动，88 小时跑完；Lean 形式化再花 17 小时。全程 490 万条消息，产出约三千亿 token。HN 上有人按 Astra 的 API 牌价一算：一千五百万美元上下。史上最便宜的千禧年难题解法，顺便也是最贵的一次推理账单。

给个体量感：一位多产数学家一生写出上千页论文已属罕见。这一晚的产出是 225 页严格证明，外加能把每一步编译通过的机器可检代码。

人类先到了半步

另一条赛道上站着 Buckmaster 和 Alpoge。前者是 NYU Courant 教授，流体方程奇点问题的多年主攻者；后者如今是 Anthropic 的研究员。两人 8 月中旬拿下 Boussinesq 和 Euler 的爆破构造，8 月 22 日完成 Lean 验证，三篇论文合计约 248 页，走的同样是「光滑外力爆破」路线。理论骨架来自 Córdoba 与 Martínez-Zoroa 的工作——Buckmaster 在声明里说，Martínez-Zoroa 的工作配得上菲尔兹奖。他们手里还押着一份超扩散粘性 NS 的爆破构造，正在等 Lean 验证，没敢先发。

注意一个容易忽略的事实：这支人类团队自己也重度用 AI——Claude 和 Codex 干重活，GPT-6 Astra 只用来写作和审计。Buckmaster 甚至把自己那份 Euler 手稿称为「AI slop」，公开为写作质量道了歉。

罗生门

真正的戏剧不在数学，在时间线。OpenAI 说这个项目 9 月 1 日启动。Buckmaster 的声明里甩出了一封 9 月 3 日的邮件：OpenAI 后来向他们承认，第一发 prompt 是在 B&A 工作的消息传到之后才发出去的。

9 月 6 日，OpenAI 的 Bubeck 与 Buckmaster 通了三次电话。按 Buckmaster 的说法，他先被告知「人工干预极少」，通话中对方改口：整支团队、多轮尝试、prompt 本身就是用 Codex 写的、「算力多到离谱」。他还指控对方两次要求把 Alpoge 从作者名单里拿掉，并留下一句「你为什么要毁掉自己的职业生涯」。Bubeck 的公开回应只有一句：指控「不实且煽动性」。

数据那笔账更微妙。OpenAI 承认「无法排除去标识化的使用数据帮助改进了我们的模型」；Buckmaster 问 Codex 会话是否进了训练集，没有等到回答。OpenAI 同时声明：无意认领千禧年奖。截至目前，只有一方拿出了文件——那封 9 月 3 日的邮件，全文可查。

数学界的判词

Terence Tao 在 9 月 7 日的博文里给了「remarkable achievement」，并认可了那个技术核心：把高频修正推入不稳定方向、再归约为不稳定 ODE 调制系统，这一步是真东西。至于无外力的 NS，「还没到」，但他补了一句：可行，且不远。克雷研究所主席 Bridson 的表态停在「激动人心的一天」。

质疑有先例背书。2025 年 12 月，前 DeepMind 总监 Budden 宣称拿到端到端 Lean 证明，事后无效，赌局在 1 月兑付。这一次的区别在于仓库公开、任何人可复验——编译器不参与江湖。

HN 上最锐利的一条测试来自网友 nairboon：让模型独立解决一个不与人类先行工作撞车的千禧年难题，比如 Yang-Mills。目前没有人敢接这一单。

奖金大概率还在桌上

克雷规则：权威期刊发表，社区两年接受，委员会全票。最快 2028 年才见分晓，一百万美元大概率原地不动。Buckmaster 把这一晚称作「深蓝对卡斯帕罗夫的时刻」。深蓝赢了那盘棋，国际象棋之后又繁荣了三十年。这一晚证明的是：允许设计外力时，流体可以在有限时间里爆炸——这是侧门的胜利。正门那扇，两条赛道现在都活着，且都开到了全速。

八天里两条赛道的交错，值得单独看一眼：

下一个观察哨有两个：B&A 押着的那份无外力方向构造何时通过 Lean；以及 OpenAI 敢不敢接 Yang-Mills。

信源：OpenAI《On the Navier–Stokes Millennium Prize Problem》及论文、Lean 仓库 openai/NavierStokesAndEuler；Tristan Buckmaster 声明（cims.nyu.edu/~tristanb/statement.pdf）及 B&A 三篇预印本；Terence Tao 博文（mathstodon，9 月 7 日）；克雷数学研究所官方问题陈述 PDF；Hacker News 讨论串。

#AIforMath #NavierStokes #千禧年难题 #机器学习