9 月 8 日，OpenAI 发了一篇研究博文：它的内部系统给出了 Navier–Stokes 方程的「奇性」证明——一道悬置了大约 90 年的千禧年大奖难题（Millennium Prize Problem）。让我反复读的不是数学结论本身，而是两个数字：约 1 万个并发 agent、一周约 3000 亿输出 token（按现价约 2250 万美元算力，TechCrunch 的估算）。以及一桩至今还在发酵的「谁先解出」学术纠纷。这篇把来龙去脉讲清楚。

先说清楚这个问题

背景：2000 年，Clay 数学研究所公布了七道「千禧年大奖难题」，每道悬赏 100 万美元。Navier–Stokes 存在性与光滑性（existence and smoothness）是其中之一。

Navier–Stokes 方程（NS）描述流体的运动，飞机设计、天气预报、血流模拟都用得到。它把流体当成连续介质，而不是一分子一分子地追踪。

悬而未决的问题是：从一个「光滑」的初始状态出发，流体会不会在有限时间内出现「奇性」（singularity）——也就是速度无界增长？方程里的粘性项本来倾向于让运动变平滑，这种「有限时间吹破」（blow-up）是否可能，90 年来没人能给出答案。1934 年 Jean Leray 证明了弱解存在，但「解是否永远光滑」留到了今天。

问题的官方表述（Fefferman 版本）里，选项 A/B 对应能导出「证明」的特殊形式，C/D 对应能导出「反证」的形式。OpenAI 的结果解决的是 C（连带 D）：从静止出发、施加光滑外力，奇性确实可以在有限时间内出现。

系统是怎么做到的

OpenAI 在博文里写明：这项工作的主体是一个「比 GPT-6 Astra 强得多的内部模型」，8 月 28 日开始训练，训练仍在继续。时间线：

• 09-01：听到「有两道千禧年难题被解决」的传闻（后来确认与 Anthropic 数学家的并行工作有关），随即启动对该内部模型的全部千禧年难题评测
• 多智能体系统：agent 可以读缓存的互联网、可以跑代码，分成组并组内通信；NS 一组的规模约 1 万个并发 agent
• 交叉授粉：用 Codex 把各组的「最有用的中间结论」汇总，再喂回去作为后续 prompt
• 09-05（周六）：第一个 agent 启动约 88 小时后，NS 组「到达」了结果
• 09-06：GPT-6 Astra 花 17 小时完成 Lean 形式化与验证，形式化证明已放到 GitHub

算力规模值得留意：全部尝试的题目合计 490 万条消息、约 3000 亿输出 token（TechCrunch 按 Astra 定价折算约 2250 万美元）；NS 一题占 270 万条消息、约 1300 亿 token。顺带一提，Euler 方程正则性问题的无外力版本也被解掉，大约 100 个 agent、50 小时。

证明的形状其实很具体：吹破的结构是一个向内螺旋、沿轴拉伸的涡旋，「像一根被拉长的意面」。中心区域越缩越小、越转越快，但总能量保持有限——加速、压力、粘性各项都变得很大，却精确地互相抵消。这种「精细平衡」（detailed balance）让光滑的外力与无界的速度得以共存。

争议：「fought dirty」

这是故事最有意思的部分。

同一天，NYU 数学系教授 Tristan Buckmaster 与 Anthropic 的数学家 Levent Alpöge（这项研究不是 Anthropic 的职务行为）公布了三项证明，其中一项是 NS 问题的初步结果。两人工作中主要用了 Codex 和 Claude。Buckmaster 在声明里写道：「关于我们进展的信息被传给了 OpenAI。」

他指出的疑点：OpenAI 走的技术路线——光滑外力路线（即选项 C/D）——正是他和 Alpöge「悄悄选定攻击」的路线，「据我所知几乎没有别的人在做这个方向」，而且「这不是把题面丢给模型、几天就能碰到的方向」。OpenAI 那边则是「整个团队」加「巨量算力」，第一条 prompt 发出时点，是「关于我们的工作信息传到 OpenAI 之后的几天内」。

更私下的细节：按 Buckmaster 的说法，OpenAI 数学家 Sébastien Bubeck 曾要求他在一个「妥协方案」里去掉 Alpöge 的署名；Bubeck 想公开纠纷时，得到的回答是「你为什么要毁掉自己的职业生涯？」以及「如果你不想让我客气，那我也可以不客气。」

技术层面的核心是数据通道：Buckmaster 大量使用 Codex 做研究，而 OpenAI 保留了用 Codex 交互训练模型的权利（用户可 opt-out）。模型在面对相似问题时，完全可能「复述」出他做过的工作。OpenAI 的回应：

我们（研究者和 agent）在他们公开发表之前，没有任何途径看到他们的工作——特别没有调取任何特定用户数据来解决这个问题。虽然不太可能，但我们不能排除：来自他们产品使用的去标识化数据，帮助改进了我们的模型。不过我们的证明差异很大，甚至在 Euler 问题上证明的具体结果也不同（有外力 vs 无外力）。

OpenAI 同时明确：不打算为这个结果申请千禧年大奖。

我拿到的两个信号

第一，「研究加速」（research acceleration）不再只是口号。一周的 agent 研究就能产出过去要一个数学家花职业生涯去追的结果。对工程师来说有个更直接的看点：Lean 形式化验证这一步，让 AI 给出的证明落在「可机器检验」的地基上——这比新闻稿可信得多。

第二，学术竞争的激励结构正在被改写。路线不神秘、算力不对等、信息会在 lab 之间漏出。当「谁先解出」开始取决于算力而非洞见，署名与优先权的规则可能需要重写；「opt-out 是否真实有效」也会变成一个真问题。

建议读者盯住两样东西：Lean 仓库（形式化证明可以被机器核对），以及 OpenAI「下一个模型」的节奏——这篇博文本质上是它的预告片。

来源：OpenAI：On the Navier–Stokes Millennium Prize Problem · TechCrunch：OpenAI fought dirty on career-making math problem, says NYU mathematician · Buckmaster 声明 · Lean 形式化证明