OpenAI 造出了一个会炸的流场，并交了 Lean 验证

七道千禧年大奖难题里，纳维–斯托克斯是唯一一道与日常物理直接相关的。方程本身自 19 世纪就写下来了，被用来算飞机的升力、河流的湍流、心脏里的血流；没人怀疑它管用，但没人能证明它的解永远不会失控——三维不可压缩情形下，一个光滑的初值会不会在某个有限时刻炸出无穷大。

答案是会，而且长得像一根面条

OpenAI 给出的解是构造性的：它造出了一个会爆破的具体流场。按其描述，那是一个向内旋进的涡旋，在收缩过程中被不断拉长，官方自己的类比是意大利面。整个过程中流体的总能量保持有界——这一点是关键，否则「炸掉」就成了平凡结论。

光有论文不够。OpenAI 同时提交了 Lean 形式化版本并通过验证，也就是说这串推理在形式系统内部无误这件事，是机器确认的，不依赖任何人读没读懂。这是近年数学与 AI 交叉最实际的一处变化：结论的可信度和作者的声望脱钩了。

一万个智能体开会 88 小时

值得单独记的是资源账。据 OpenAI 披露：

• 约 1 万个并行智能体参与求解；
• 彼此传递约 270 万条消息；
• 产生约 1300 亿输出 token；
• 主证明约 88 小时成形，Lean 形式化与验证再花约 17 小时。

执行任务的不是已发布的 GPT-6 Astra，而是一个未公开的内部模型，OpenAI 称其能力显著更强。1300 亿输出 token 意味着这次求解有一个可以标价的成本——按当下前沿模型的公开单价粗算，仅输出侧就是七位数美元起步，还没算一万个智能体互相通信时反复读进去的上下文。

这个数字比证明本身更能说明方法论上的转折：过去是一个人想很久，现在是一万个实例并行地想很短的时间，再由形式化验证器把对的那条路捡出来。前者靠洞察，后者靠搜索加过滤。

算不算解开，还没定

Lean 能确认推理无误，但不能裁定这个命题是否满足克雷数学研究所对该问题的每一条设定——尤其是「带光滑外力」这个前提在原问题的正式表述里如何处置。多家报道都指出，数学界仍需要时间逐条检视这份论证。OpenAI 明确表示无意申领奖金，某种程度上也绕开了这道判定。

同一周还有另一组结果：纽约大学教授 Tristan Buckmaster 与 Anthropic 研究员 Levent Alpöge 证明了受迫欧拉方程的有限时间爆破，陶哲轩称之为「一项了不起的成就」。OpenAI 起初以为对方解的是同一道题并提议联合发布，弄清是受迫欧拉后承认了对方在该问题上的优先权。Buckmaster 随后对 OpenAI 在署名安排上的做法提出了公开批评，这部分目前是单方面陈述。

把这两条线放在一起看，能看出这一年最真实的变化：几个月前争论的还是模型能不能做对奥数题，现在争的已经是谁先做出的、以及谁能署名。