AI 真的解开纳维—斯托克斯了吗？先分清证明、形式化与公认

luyuanhong

AI 真的解开纳维—斯托克斯了吗？先分清证明、形式化与公认

原创  AI 研客  AI 研客  2026 年 9 月 9 日 07:54  广东

今天可以确认的，是一份公开的候选证明和形式化仓库；还不能确认的，是数学界已经完成验证并公认难题解决。

9 月 8 日，OpenAI 公开了一份 166 页的论文《Finite Time Blowup for Navier–Stokes》，以及配套的 Lean 形式化仓库。官方称，一个正在训练、能力显著超过 GPT-6 Astra 的内部模型，通过大规模并发代理得到了纳维—斯托克斯方程的一个有限时奇点构造。

这条消息同时涉及偏微分方程、AI 代理、形式化验证和数学共识。要判断它的分量，关键不是把“有 Lean 代码”简化为“已由计算机证实”，而是分层问四个问题：论文构造了什么，其物理图像是什么，形式化覆盖到哪一层，外部数学共同体还需做什么。

01｜论文声称证明了什么


OpenAI 候选证明论文首页，摘要声称构造了有限时速度无界、动能仍有界的解

纳维—斯托克斯方程用来描述黏性流体。千禧难题问的核心之一是：在三维不可压缩条件下，从光滑初始状态出发，解是否永远保持光滑，还是可以在有限时间出现奇点。奇点在这里指速度或相关量失去有界性，不是现实中真有流体达到无穷大速度。

论文的 Theorem 1.1 声称：对任意正黏度，都能构造出一个三维不可压缩流。它从静止状态开始，外力是光滑且在空间和时间上都有紧支撑；在奇点时刻之前，速度场保持光滑，总动能保持有界，但速度的最大值趋于无界。作者认为，这建立了 Clay 官方题面中的选项 C，并因紧支撑构造同时得到周期区域上的选项 D。

这里的限定很重要：它不是对每一种流体都声称必然爆破，而是给出一个符合题面条件的反例构造。如果构造和所有估计成立，它表明黏性的平滑效应并不能在所允许的外力条件下排除所有有限时奇点。

02｜这个奇点构造如何工作


论文图 1：内核在三个时刻逐步收缩，旋转速度增大。图为作者机制示意

论文首先构造一个轴对称的旋涡内核。随着奇点时刻接近，流体向旋转轴线内卷，同时沿轴向向上与向下流出。它的径向尺度比轴向尺度收缩得更快，中心区域因而变成越来越细的柱体。流体越靠近轴线，角动量运输使旋转速度增大；与此同时，内核体积收缩得更快，所以速度无界与总动能有界可以并存。

真正困难的部分不只是让速度增长。对任意先指定的速度和压力场，总可以把方程中未平衡的剩余项当成外力；但 Clay 题面要求外力也要足够光滑。如果旋涡本身的剩余项也在奇点处爆掉，这个构造就不合格。

作者的处理是在内核外缘的环形区域加入两类空间振荡脉冲。这些脉冲从背景剪切中获得能量，它们的非线性动量通量用来抵消背景场剩余中的奇异部分。随后再通过高阶修正，使最终留下的外力在奇点时刻仍可光滑延拓。可以把这个证明的主线理解为：先设计会收缩和加速的旋涡，再用可控振荡去修复方程中不允许的剩余。

03｜AI 找到证明的方式同样值得关注

OpenAI 的发布文章称，团队在 9 月 1 日启动对多个千禧难题的探索，不同代理组分别研究证明与反例选项。最终找到纳维—斯托克斯构造的组，规模约为 1 万个并发代理。从启动到得到解决方案约 88 小时，随后用 GPT‑6 Astra 完成 Lean 形式化和验证又用了 17 小时。官方给出的资源计数是，该问题涉及约 270 万条代理消息和 1300 亿输出 token 。

这里有两个可复用的方法信号。第一，并发不只是同一提示重复一万次，而是将题面的不同分支、尝试和中间结果分组推进，再用 Codex 汇总有用思路。第二，计算成本本身就是结果的一部分：这不是今天普通订阅者用一次对话就能复制的能力。上述数字都来自 OpenAI 自述，目前不能当成外部独立复现记录。

04｜有 Lean 形式化，为什么仍需外部审核

Lean 可以让证明中被编码的定义、引理和逻辑推导由内核逐步检查。这比只有自然语言论文更容易发现“这一步并未从前提推出”之类的空洞。但形式化的强度依赖于具体被编码的命题、定义、公理与库环境。外部审核还要核对：形式命题是否精确对应 Clay 题面，有无未被形式化的桥接步骤，分析假设和函数空间是否一致，以及代码与论文是否表达同一个数学结果。

形式验证解决的是“给定这套形式化输入，推导是否通过”，学术共识要解决的则是“这套输入是否忠实、完整地表达了原问题”。两者相互补强，但不是同一层的验证。

∞｜今天最稳妥的结论

Clay 数学研究所的现行规则很明确：它不接受直接投递的候选解法。在考虑千禧奖之前，结果必须在合格出版渠道发表，至少经过两年，并在全球数学界获得普遍接受。最终是否满足官方题面，也由 Clay 依规则决定。

因此，目前最准确的说法是：OpenAI 已经公开一份声称解决纳维—斯托克斯千禧难题的候选证明，并提供 Lean 形式化仓库；数学界和 Clay 的外部验证尚未完成。 下一步应关注的不是标题里的“AI 破解”，而是专家对关键估计、形式命题和官方题面对应关系的逐项审核。

来源

● OpenAI：On the Navier–Stokes Millennium Prize Problem
● OpenAI：Finite Time Blowup for Navier–Stokes（PDF）
● OpenAI GitHub：NavierStokesAndEuler Lean certificates
● Clay Mathematics Institute：Navier–Stokes Equation
● Clay Mathematics Institute：千禧难题官方题面（PDF）
● Clay Mathematics Institute：Rules for the Millennium Prize Problems

AI 研客