OpenAI 的 Navier–Stokes 证明：宣称了什么、谁核验过、功劳归谁

OpenAI 宣称了什么

2026 年 9 月 8 日，OpenAI 发布《On the Navier–Stokes Millennium Prize Problem》，称其内部系统给出了解析证明和 Lean 形式化，证明一团初始静止、光滑的流体在光滑外力作用下，能在有限时间内形成奇点，而能量始终有限。OpenAI 称，这“通过确立官方千禧年表述中的命题 C（以及 D），解决了 Navier–Stokes 千禧年难题”，同时写明“我们不打算为这一结果申领千禧年奖”。所用的内部模型据称“明显强于 GPT-6 Astra”，自 8 月 28 日起一直在训练中。^[S1]

论文《Finite time blowup for Navier–Stokes》共 166 页，署名只有“OpenAI”。定理 1.1：对每个 ν > 0，存在空间与时间上都紧支撑的光滑外力 f，以及 [0, 1) 上的光滑速度与压力，使 u(·, 0) = 0、动能一致有界，而 t → 1 时速度的 L∞ 范数上极限为无穷。论文据此宣称确立了 Fefferman 表述中的 (C)，并由紧支撑得到环面 T³ 上的 (D)（推论 10.6）。^[S2]

克雷的官方表述确实允许外力：(C) 要求存在满足衰减条件的光滑无散初值 u° 与光滑外力 f，使得不存在满足光滑性与有界能量条件的解。所以引入外力本身并没有越出题面。无外力的版本（光滑解是否对一切时间都存在）仍未解决；这里的外力是为维持坍缩而专门构造的。^[S7][S16]

据 OpenAI 自述：证明是怎么找到的

据 OpenAI 说，9 月 1 日（周二）听到“两个千禧年难题已被解决”的传闻后，他们让一套由内部模型驱动、相互协作的智能体系统去攻所有未解的千禧年难题，不同小组分别拿到 A/B（证明方向）与 C/D（否定方向）等不同表述。智能体可读取互联网缓存、运行代码。在一组“更容易”的问题里，约 100 个智能体用约 50 小时解出了无外力的 Euler 爆破问题；此后 OpenAI 把资源集中到 Navier–Stokes，把 Euler 的解答作为提示交给智能体，并用 Codex 汇总各组的中间结果、再分发回去。解出 Navier–Stokes 的那一组约有 1 万个并发智能体，9 月 5 日（周六）得出结果，距首批智能体启动约 88 小时；随后 GPT-6 Astra 又用 17 小时完成 Lean 形式化与验证。所有问题合计，智能体共发出 490 万条消息、约 3000 亿输出 token，其中 Navier–Stokes 一题占 270 万条消息、约 1300 亿 token。^[S1]

以上都是 OpenAI 自己的陈述，没有公开日志可供核对。据 Buckmaster 的声明，他起初被告知模型“只拿到了题面”，Alpöge 则从 Bubeck 那里听说人类投入“很少”；通话过程中，OpenAI 团队陆续发来更正，事情才清楚：其实有一整支团队参与，工作先从无外力问题和 Euler 等较容易的问题做起，展示给他的提示词本身也是让 Codex 写的。^[S1][S10]

机器究竟核验了哪句话

OpenAI 的 Lean 仓库（Lean 4.34.0-rc2 + Mathlib，Apache-2.0）没有自己写题面，而是改编了 Google DeepMind Formal Conjectures 项目里早已存在的 Navier–Stokes 形式化，并附上 Comparator 挑战文件，任何人都可以检查所证定理的类型是否与参考命题一致。我们把 OpenAI 的 NavierStokes/ComparatorDefinitions.lean 与 formal-conjectures 在 8bf45ed 提交的原文件逐行比对：改动只有：导入、命名空间、记号改为局部、去掉分类属性、改写模块说明，以及删去 (A)–(D) 四个以 sorry 占位的定理；结构定义在数学上没有任何改动。ComparatorSolution.lean 中 (C) 定理的陈述，与原文件留待证明的 (C) 逐字相同。^[S4][S5]

这正是这次发布的新意：判断“证的是不是那道题”，不必再靠通读 166 页；一次 diff 就能表明，所证命题与一个事先写好的形式化命题一致。但 diff 不单独完成全部语义对应的审查：那个形式化命题是否把克雷 (C) 的每一项要求都写对了，仍要靠人去读。机器核验给出的“成立”，也是相对于这个形式化命题、Lean 的公理和可信内核而言。文字论文是否正确、是否可读，是又一个问题。

功劳归谁：三种说法

到 9 月 7 日 Tao 撰文介绍时，Buckmaster（纽约大学）与 Alpöge（Anthropic 员工，以个人身份参与）已经公开了三项带光滑外力的有限时间爆破结果：不可压多孔介质方程、Boussinesq 方程与三维不可压 Euler 方程，均附 Lean 形式化。Buckmaster 把这条路线的基本思想归功于 Córdoba 与 Martínez-Zoroa 多年来的外力爆破构造，并说他和 Alpöge 是在大语言模型的大量帮助下，才把这一方案推进到光滑外力和 Euler 方程；他列出的工具包括 Anthropic 的 Claude 与 OpenAI 的 Codex（GPT-5.6 Sol，后来还有 Astra）。Tao 在 9 月 7 日的博文中也把这条路线归于 Córdoba 与 Martínez-Zoroa，并认为 Alpöge–Buckmaster 的变体“很有可能”也能推广到 Navier–Stokes。^[S10][S11]

OpenAI 的论文引用 Córdoba–Martínez-Zoroa（及 Zheng）的工作，称其确立了“跨尺度放大”的奇点形成策略，并说自己的构造同样利用动力学放大，只是被放大的扰动扮演的角色不同；论文没有提到 Alpöge 与 Buckmaster。OpenAI 的博文“承认他们在外力 Euler 问题上的优先权”，同时强调两边的 Euler 结果并不相同：对方的有外力，OpenAI 的无外力。至于 Navier–Stokes 本身，OpenAI 没有把功劳归给任何别人。^[S2][S1]

Buckmaster 写道，“外力”这个词在他看来是“一个刺眼的危险信号”：经由光滑外力（Fefferman 表述中的 c、d）通向克雷问题，正是 Córdoba 与 Martínez-Zoroa 开辟、他与 Alpöge 悄悄选定的路线，“几乎没有别人在做”；把题面交给模型，几天之内也不会走到这个方向。他说 OpenAI 最终承认，首个提示词是最近几天、“在关于我们工作的信息传到 OpenAI 之后”才发出的；他问模型是否用他们放进 Codex 的草稿训练过，没有得到回答。他同时写明：他没看过 OpenAI 的证明，不知道模型做了什么，也不知道他们的数据是否被用过，“我不指控任何人”。^[S10]

OpenAI 博文中的回应前后有两个版本。TechCrunch（9 月 8 日）与 The Next Web（9 月 10 日）引用的原话是：“虽然可能性不大，但我们无法排除这种情况：来自他们使用我们产品的去标识化数据，帮助改进了我们的模型。”我们 9 月 26 日读到的现行版本则改成：“经调查，我们已确认 Buckmaster 在本次公告前两个月内的 Codex 提示……不可能以任何方式影响该系统，包括通过训练。”页面没有注明这处改动，调查的方法和材料也都没有公开。^{[S12][S13][S1]}

署名问题同样有两套说法。Buckmaster 说，Bubeck 在 9 月 6 日的通话中两次表示希望把 Alpöge 从作者名单中去掉；听说他打算公开此事，Bubeck 回了一句：“你为什么要自毁前程？”Bubeck 在 X 上发帖（据 The Next Web 转述），否认曾要求把 Alpöge 从其自身工作的署名中去掉，称“要是 Levent 不是 Anthropic 员工就简单了”那句话，针对的是请两人合写 OpenAI 证明的提议；他也为“前程”那句话道了歉。这是双方对私下通话各执一词的陈述，没有经过任何独立程序检验。^[S10][S13]

谁核验过，核验了什么

这里其实是四个不同的问题，证据强度各不相同：机器检查是否通过；形式化命题是否对应克雷的表述；自然语言论证是否经过审阅；以及优先权与奖项的评估。前两个可以用代码回答一部分，后两个只能靠人和程序。下面按这个顺序记录。

OpenAI 自己。

仓库的 formalization.yaml 记录 sorry 数为 0，主定理只依赖 Lean 的三条标准公理（propext、Classical.choice、Quot.sound），形式化由 GPT-6 Astra 经 Codex 完成，审查状态写的是“self-assessed”（自评）。^[S4]

一个外部 GitHub 账户。

CrystalArchitect/navier-stokes-lean-check 报告：在 macOS 上从源码构建，11,251 个任务成功，两条主定理的公理列表不含 sorryAx；命题定义与 formal-conjectures 逐字节一致。它也说明，没有运行 nanoda 独立内核重放（Comparator 依赖的 landrun 只能在 Linux 上运行），文字论文是否正确也不在检查范围之内。账户背后是谁不得而知。我们读了它的 README，没有自己构建这个 Lean 工程；上文的命题比对是我们自己做的。^[S6]

数学家：以它为基础做研究，不等于审过它。

Constantin、Ignatova 与 Vicol 的预印本（9 月 17 日）证明：具有该构造两项关键特征（角向平均满足特定的各向异性 Type II 界；在坍缩核心区域内严格轴对称）的解，只要外力在空间上实解析，在假定的奇点处其实是正则的。摘要由此得出：在 OpenAI 的构造中，以及在任何具有这两项特征、且外力直到奇点时刻都保持 C² 有界的构造中，外力既不能在奇点附近恒为零，也不能在空间变量上（对时间局部一致地）实解析。注意这是“在奇点附近的一个邻域内恒为零”被排除，不是说外力在奇点这一点上不能为零。这为结果划定了边界，但并不是对其正确性的审稿。另有预印本把 OpenAI 的构造当作已知结果，由此推导密度结论。Tapio Schneider 在 Tao 博客的客座文章（9 月 23 日）中写道，形式化验证支持这一证明是正确的，但数学家们仍在消化它。^{[S14][S15][S16]}

克雷研究所：尚未开始。

克雷 9 月 11 日的声明说，它同样为“Navier–Stokes 问题看来已被解决”的消息感到振奋；评估成果、确定功劳的流程由奖项规则规定，而且“刻意从容不迫”。规则要求：解答须发表在合格的出版物上，发表后至少满两年，并在全球数学界获得普遍接受，然后再由克雷判定它是否回答了官方问题；克雷不受理直接投稿。OpenAI 的论文目前只挂在自己网站上，而且 OpenAI 表示不申领奖金。^[S8][S9]

为什么是第 2 级

这个证明是存在于软件和文本中的结果：一篇论文，加一个能编译的 Lean 工程。按本站的证据阶梯，证明属于“算出来了”这一级；机器核验让这一级更扎实，但不会把它推到“对照已有证据检验”。Lean 检查的对象是第三方事先写好的命题，这是少见的长处；而就我们截至 9 月 26 日所能找到的，文字论证公开的评估只来自作者一方。

三件事要分开记

谁宣称：OpenAI，以公司名义、无个人作者。谁核验：Lean 内核（OpenAI 自评，外加一次身份不明的外部重建），检查的是与事先写好的形式化命题的对应；截至 9 月 26 日，未找到对文字论证的公开独立审稿报告。功劳归谁：OpenAI 未把 Navier–Stokes 的功劳归给别人，只承认 Alpöge 与 Buckmaster 在外力 Euler 上的优先权；Buckmaster 把整条路线归功于 Córdoba 与 Martínez-Zoroa；克雷的裁定尚未开始。把这三件事写成一句“AI 解决了千禧年难题”，就是把三种强度悬殊的证据压成了一种。

形式化把“证对了没有”和“证的是不是那道题”分开

以往，一项重大证明主张更难核对的往往是后者：定理是不是悄悄比宣称的弱。这次借用了第三方事先写好的命题，这一风险用一次 diff 就能排除。但它排除不了来源问题，因为来源是关于训练和交互过程的主张，外人无从查看。

规模成了研究工具本身的一部分

约 1 万个并发智能体、88 小时、约 1300 亿输出 token：能以同样规模复现这一搜索过程的机构寥寥无几。谁都能复现的是 Lean 检查；外界谁也复现不了的，是产生证明的过程。^[S1]

外部把关正在形成，但没有决定权

9 月 21 日，九位数学家宣布成立“数学与人工智能咨询小组”（AGMAI），设在普林斯顿高等研究院。起因是 OpenAI 找到其中部分成员，想组建一个外部顾问委员会，他们商定改为成立独立小组。小组眼下的任务，是就 OpenAI 如何协调发布其内部模型据称产出的“大量重要数学成果”提供建议；成员不领报酬，小组对任何 AI 公司都没有决策权。成员 Martin Hairer 在随后的客座文章中写道，近几个月 AI 公司发布高知名度数学成果的方式“远未达到可接受的数学惯例”。^[S17][S18]