9 月 8 日,OpenAI 在官网发布文章《On the Navier–Stokes Millennium Prize Problem》,宣布其内部模型产出了一个证明:三维不可压缩 Navier–Stokes 方程的解可以在有限时间内从光滑初始条件发展出无界速度。这是克雷数学研究所 2000 年悬赏一百万美元的七个千禧年大奖难题之一,此前已悬置约九十年无人完整解决。证明附带了 Lean 形式化版本,由 GPT-6 Astra 花费 17 小时完成机器验证。

同一时间线上的还有第二条线:纽约大学数学教授 Tristan Buckmaster 与 Anthropic 研究员 Levent Alpöge 在 9 月 8 日深夜公开了三篇预印本,给出带光滑外力的三维不可压缩 Euler 方程有限时间爆破(blowup)证明,同样通过 Lean 验证。两边的工作指向同一族方程,方法同源,发布时间相差不到一天,而两条团队之间的接触过程本身也成了一起公开争议。
问题在问什么:方程会自己崩溃吗
Navier–Stokes 方程写的是牛顿第二定律在流体上的版本。它把流体当作连续介质,不追踪单个分子,用速度场、压强场和黏性项描述液体与气体的运动。飞机设计、天气预报、血流动力学都在用这组方程。
数学层面悬而未决的问题是:给定光滑的初始状态,方程的解是否永远保持光滑。所谓奇点(singularity),指流体速度在有限时间内增长到无界。真实的流体不可能无限快,所以奇点意味着连续介质近似在这一点失效,要继续描述系统就只能逐个追踪粒子。1934 年 Jean Leray 证明了广义意义上的解存在,但解是否始终光滑,此后一直是核心悬念。2000 年克雷数学研究所把它列入七个千禧年问题,每一种表述版本都对应一百万美元奖金。
这个问题有两个方向:证明「解永远光滑」(存在性与光滑性)或者证明「解会爆破」(构造出反例)。OpenAI 走的是第二条路,建立了克雷官方表述中的备选(C)和(D)。
证明本身:一个把自己拉断的涡旋
根据 OpenAI 公布的论文《Finite Time Blowup for Navier–Stokes》(166 页),构造的核心是一个涡旋:流体绕轴旋转,向内螺旋的同时被轴向拉伸,越来越像一根被拉长的意面。中心区域在收缩的同时加速,速度冲向无界,但总动能始终有限,满足物理约束。
技术上最难的部分是让爆破由流体自身的运动产生。方程里的加速度、压力梯度、动量输运、黏性各项都必须同时变得极大,又以精确的方式相互抵消,只留下一个保持光滑的外力。论文的定理陈述是:对任意正黏性系数,都存在一个紧支撑的光滑外力,使从静止出发的解在有限时间内速度的无穷范数发散,而动能全程有界。

OpenAI 官方配图展示了这个局部不可压缩运动的快照:橙色标记更快的角向旋转,青色标记更慢的旋转,环向速度还依赖半径,轨迹呈现向内螺旋与轴向拉伸。
两条团队,两条路线
Euler 方程是 Navier–Stokes 去掉黏性项后的极限情形。Buckmaster 与 Alpöge 解决的是带外力的 Euler 正则性问题,OpenAI 的智能体群体则顺带解决了无外力版本的 Euler 爆破,约 100 个智能体协作约 50 小时完成。两组工作都建立在 Diego Córdoba 与 Luis Martínez-Zoroa 多年发展的「forcing」(强迫项)思路上:利用克雷问题表述中一个长期被多数专家默认无关紧要的项来打破方程。
Buckmaster 在公开声明中把时间线写得很具体:8 月 15 日拿到 Boussinesq 与 Euler 的光滑外力爆破结果,8 月 22 日完成第一份 Lean 验证。9 月 3 日起,围绕「Anthropic 解决了重大数学问题」的流言,他与 OpenAI 的 Sébastien Bubeck 通话,随后得知 OpenAI 内部模型已产出带强制项 Navier–Stokes 爆破的约百页证明。他在声明中称 Martínez-Zoroa 应得菲尔兹奖,并直言两人论文的行文「只能被称为 AI slop」,因为外部压力没时间打磨。
OpenAI 一侧的叙述补充了工程细节:8 月 28 日起训练一个内部新模型(官方称其能力显著超过 GPT-6 Astra,训练仍在进行);9 月 1 日受流言启发启动评估,把全部千禧年问题分发给不同智能体小组,每个小组拿不同的问题表述变体;产出的那个小组规模约一万个并发智能体,智能体可以读缓存的互联网、跑代码、组内通信;9 月 5 日拿到解答,距首批智能体启动约 88 小时;全项目智能体互发 490 万条消息、消耗约 3000 亿输出 token,其中 Navier–Stokes 一题占 270 万条消息、约 1300 亿 token。官方还说明,9 月 6 日完成 Lean 验证后主动联系 Buckmaster 与 Alpöge 提议联合发布,并确认两组证明差异显著,Euler 问题上连命题本身都不同(带外力与不带外力)。
Lean 验证:AI 数学的质检环节
两边的证明都走了同一条质检路径:先由模型或人机协作产出证明,再翻译成 Lean 定理证明语言做机器核验。OpenAI 的 Navier–Stokes 形式化花了 17 小时;Buckmaster 一侧 8 月 22 日完成首份验证,第三个结果(低耗散 Navier–Stokes)因验证未完成而暂缓发布。
这条流程正在成为 AI 数学科研的标配:模型负责探索与构造,Lean 负责排除幻觉与漏洞,人类数学家负责方向判断与最终把关。Buckmaster 声明里对行文质量的抱怨与对结果的笃定同时存在,恰好说明当前分工的边界:结论的可信度由形式化系统背书,叙述质量仍然是短板。
争议与边界
围绕这次发布有三个需要分开的事实层。第一,数学结果本身:两个团队的预印本与 Lean 代码都已公开,任何人可以检验。第二,奖金归属:OpenAI 明确表示不申领千禧年大奖,克雷研究所的官方页面也未更新结论;且其构造依赖外力项,属于克雷表述中的特定备选。第三,过程争议:Buckmaster 声明中提及通话里的署名安排与一句「Why would you ruin your career?」,OpenAI 未回应媒体置评请求,这一段目前只有单方陈述。
对普通开发者来说,这轮发布里最可复用的部分不在方程,而是那套多智能体科研工作流的参数:问题拆成变体并行分发、小组规模按难度伸缩(Euler 100 个、Navier–Stokes 一万个)、Codex 汇总各组洞见做交叉授粉、中间结果直接写进后续 prompt、Lean 做最终闸门。88 小时、3000 亿 token 换一个九十年悬案的候选解,这套配置清单比结论本身更容易被复制到其他领域。
来源:OpenAI 官方博客及论文 PDF、Tristan Buckmaster 声明(NYU)、Scientific American、Unite.AI