88 小时、一万个智能体与一道千禧年难题
声明、Lean 证明，与其背后的功劳之争

OpenAI 究竟声明了什么

一套内部系统产出了一份解析证明与一份 Lean 形式化，表明：一团初始光滑、静止的流体，在受到光滑外力时，可以在有限时间内发展出奇点，而全过程其总能量始终有界。OpenAI 称这确立了 Charles Fefferman 官方克雷表述中的命题 “C”（以及“D”）——即对全局正则性的反证，而非证明解永远保持光滑。它明确表示不会申领百万美元大奖。

本报告坚持的一条纪律：三种不同状态

我们的判断

• 若成立，其数学重要性：里程碑级——迄今涉及 AI 的最重大结果，也是继庞加莱猜想之后第二个被回应的千禧年难题。
• 当前确定性：中等，偏向“待验证”。机器核验大幅抬高了下限，但命题等价性、两条团队路线之间的关系以及署名归属仍在厘清中。
• 范式信号：强。无论这份具体证明能否站住、署名人是谁，“大规模并行智能体搜索 + 形式化验证”已被证明能作用于一道开放的前沿难题——而不只是有已知答案的题。
• 近期可产品化程度：低。这是一次耗资数百万美元、资本密集、且外部无人能访问其模型的运行——是一台科学仪器，而非按次调用即可购买的 API 能力。

• 并非“OpenAI 先发、他人追赶”：另一方关键的、经 Lean 核验的突破可追溯到 8 月中下旬；OpenAI 自己把起点定在 9 月 1 日的传闻。两支团队几乎同时撞上一条非常狭窄、小众的路线。
• 即便在热身阶段，他们证明的也不是同一命题：在 Euler 上，Buckmaster–Alpöge 证明的是受迫（光滑外力）版本，OpenAI 智能体证明的是无外力版本。在 Navier–Stokes 层面，只有 OpenAI 声称得到完整结果；另一方得到一份未验证的亚耗散 NS 结果，并选择不发布。
• 在“同期工作”一节，OpenAI 在三维 Euler 上让出优先权——“我们承认他们在受迫 Euler 上的优先权并向其祝贺”——同时把 Navier–Stokes 归于自己。

3.1 一段话讲清问题

Navier–Stokes 方程把牛顿第二定律（F=ma）应用于被视为连续介质（而非一团分子）的流体，支撑着飞机设计、天气预报与血流研究。方程由 Navier（1822）与 Stokes（1845）写下，一个基本问题却始终未解：给定一团三维、初始无比光滑的不可压缩流体，解会永远规规矩矩，还是某个无穷小流块会在有限时间内无界加速——形成奇点？黏性通常会抑制运动，这正是难点所在：方程必须靠流体自身的动力学爆破，而不是被人为塞进一个无穷大力。OpenAI 的答案是：会——有限时间爆破。

3.2 为什么花了九十年

Quanta 把最后一道坎讲得最清楚：Córdoba 与 Martínez-Zoroa 构造出无穷序列的非奇异“层”，并把它们组合成一个包含奇点的无限级联。每一层都光滑，但过去把它们叠加后，外力函数会带上不理想的性质——不满足克雷对外力必须光滑的要求。两支 AI 团队都声称跨过的一步，正是造出一个既产生奇点、又仍留下光滑外力的级联。

3.3 爆破长什么样——以及它对工程意味着什么、不意味着什么

被构造出的对象是一个涡：它向内螺旋、像意面一样被沿轴拉伸；核心越来越细、越转越快，趋于无界，而总能量保持有限。技术上的惊人之处在于：加速度、压力梯度、动量输运与黏性都必须变得很大，却又以极高精度相互抵消，最终只留下一个光滑外力。

4.1 关键数字（官方数字与外部估算严格分开）

4.2 方法中真正新颖之处

这不是“把问题敲进模型然后干等”。不同智能体小组被分派不同命题变体——A/B（会得到正则性证明）与 C/D（会得到爆破）——以此显式对冲“押错方向”的风险。智能体可读一份缓存的互联网副本、可运行代码、可在组内通信；Codex 随后在组间“交叉授粉”，整合最有用的中间结果，把更早的 Euler 解作为提示回灌。人的角色是设计搜索空间、分解问题、编排智能体群、判断哪条路有希望，而非亲自推导。OpenAI 甚至说，其团队整体缺乏流体力学的研究级专长，“无法对数学本身做出真正有意义的贡献”——这段自述本身也应带着几分审慎去读。

4.3 Lean 保证什么——以及它替你做不了的那一项核查

Lean 是一个交互式证明助手：命题与证明用形式语言写出，软件检查每一步推理。一份能编译、不用 sorry 占位、且只依赖 Mathlib 与标准公理的证明，在其所选定义与公理之内拥有闭合的逻辑链。这比一份等待评审的手写预印本可靠整整一个档次——也是它与 NS“证明墓地”的本质区别。

• ① 命题正确性不会自动成立：“光滑外力”“有限能量”“整个 ℝ³ / 环面”的形式化编码，是否与 Fefferman 的 C/D 条件精确吻合，必须由外部专家逐行核查。OpenAI 声称在 ℝ³ 与三维环面上都覆盖了 C 和 D；这恰恰是需要审计之处。
• ② 它既不证明物理意义，也不证明重要性：机器对结果意味着什么保持沉默，这要由人赋予。
• ③ 它尚不是共同体接受：外部数学家还没有独立构建并审计该仓库。形式化让结果可审计；可审计 ≠ 已被接受。

5.1 另一支团队做了什么

纽约大学教授 Tristan Buckmaster 与数学家 Levent Alpöge——后者受雇于 Anthropic，却极力强调自己以个人身份参与、无机构项目、工具费用出自 Buckmaster 的科研经费——使用 Anthropic Claude、OpenAI Codex、GPT-5.6 Sol 以及后来的 Astra（Astra 仅用于成文与审计），为三个模型方程取得了经 Lean 核验的、带光滑外力的有限时间爆破：不可压缩多孔介质方程（IPM，另与 Matei P. Coiculescu 合作）、二维 Boussinesq 方程组、三维不可压缩 Euler。他们还相信自己得到了亚耗散 Navier–Stokes 的爆破，但因 Lean 验证未完成、也拿不出像样成文而拒绝发布。

菲尔兹奖得主 Terence Tao（陶哲轩）在 9 月 7 日写道，称这是沿 Córdoba–Martínez-Zoroa 路线的一次“令人兴奋”/“非凡”进展，把次临界/粗糙外力一路推进到完全光滑，并判断推广到完整 Navier–Stokes“在不久的将来非常可行”、“没有根本性障碍”。他也补了一句值得记住的冷静话：求解只是代理目标，首要价值在于数学理解；缺了理解，NS 正则性问题“其内在意义……远不如大众媒体有时鼓吹的那么大”。

5.2 两支团队一览

5.3 争议的三层，按证据强度排序

第一层——“OpenAI 是否在泄露后冲刺？”（时间线大体可核查，解读各异）。Buckmaster 称两人的进展一旦泄露便被迫提前发布；OpenAI 承认自己 9 月 1 日才因“Anthropic 解决了”的传闻启动，并在 9 月 6 日完成工作后联系对方、提议同时发布且让对方先发。时间线本身大体可验证——另一方关键结果在 8 月中下旬，OpenAI 的运行在 9 月 1–6 日。

第二层——他们的私人 Codex 草稿是否被用于训练？（核心；正反均无证据；OpenAI 未完全回答）。两人把每份草稿、提示与中间产物都留在 Codex。Buckmaster 的问题从来不是“模型有没有实时读我的会话”，而是“这些会话有没有进入训练/改进流水线”。他说对方告诉他“模型不会调取用户数据”，而他追问训练一事时“没有得到回答”。OpenAI 自己的措辞是：解题时没有访问任何特定用户数据，但“无法排除源自其使用我方产品的去标识化数据帮助改进了我方模型”，尽管其认为可能性很低。

第三层——署名与所谓施压（各执一词；双方都有声明或截图）。Buckmaster 称对方曾向他提出两个方案，其中一个要他单独署名一篇 NS 论文、因 Alpöge 受雇于 Anthropic 而将其排除，并转述了“你为什么要毁掉自己的职业生涯？”之类的话。Bubeck 公开否认曾要求去掉 Alpöge，承认出于知识产权考虑说过“如果 Levent 不是 Anthropic 员工，事情会简单些”，为“糟糕的措辞”道歉并称当场收回，同时反指通话一开始就有诽谤性指控与联系媒体的威胁。Sam Altman 同样表示他本想联合发布、主动提出让对方先发并去角逐大奖，只是无法把同样安排延伸给一名 Anthropic 员工。这一层目前由相互冲突的单方说法构成；诚实的做法是把它们并排放置。

5.4 被忽略的“真正英雄”

这场争吵真正澄清的是：两支 AI 团队都站在同样两位人类数学家的肩上——Diego Córdoba（马德里 ICMAT）与 Luis Martínez-Zoroa（CUNEF）。撰写克雷原题的 Fefferman 直言“这个故事的英雄是 Córdoba 和 Martínez-Zoroa”；Buckmaster 写道，Martínez-Zoroa 凭其系列工作配得上一枚菲尔兹奖；Córdoba 则开玩笑说“我不用 AI：我有 Luis”。这个提醒很直白：AI 是沿着人类开辟的小众路线，快速冲过了最后一道技术缺口——它并没有发明这套研究纲领。

6.1 克雷规则

候选者必须同时满足三条：（i）在“合格载体”——享有世界声誉的同行评审期刊——发表；（ii）发表后至少成立两年；（iii）获得全球数学界的普遍接受。不接受直接投稿。作为参照：迄今唯一被解决的千禧年难题庞加莱猜想，从 Grigori Perelman 2002 年 11 月预印本到 2010 年 3 月授奖历时七年以上，且他本人拒领。截至撰稿，克雷官网仍把 Navier–Stokes 列为未解，研究所对 OpenAI 的声明既未接受也未拒绝；OpenAI 表示不会申请百万美元，把这次发布定位为“一个时间切片……而非终局”。

6.2 为什么学界缓慢、程序化的谨慎是对的

Navier–Stokes 是著名的“证明墓地”：不止一份宣布过的解答后来在审视下崩塌——Otelbaev 2014 年的声明就被 Tao 等人公开追踪、最终判定无法挽救。面对一份来自非传统渠道、裹着商业与优先权争议的 165 页证明，学界“独立构建 Lean、慢慢读、暂不下结论”的本能不是保守，而是让数学保持可靠的机制。

• 第一次跃迁（2024）：在有标准答案的奥赛题上达到奖牌级——考的是解题能力。
• 第二次跃迁（2025–2026 上半年）：开始碰已知的开放问题（Erdős 遗产）——考的是在人类已测绘的地形内推进。
• 第三次跃迁（2026.09）：面对没有现成路径的开放前沿，甚至要在相反方向（证光滑 vs 构造爆破）之间下注，以超大并行度搜索、再形式化验证——考的是帮助开辟新地形。

8.1 研究生产函数改变：稀缺性从“求解”移向“提问”与“编排”

当一万个智能体可以并行尝试数百条证明路径，稀缺资源便不再是苦熬冗长推导，而是另一端：把模糊的科学问题重述成机器可搜索、可验证的形态（Tao 所谓“好问题成为稀缺资源”）；设计搜索空间（A/B/C/D 变体、更易的热身、跨组授粉）；以形式化为兜底，同时由人完成最难的一步——确认“形式化问题＝真实问题”；以及把机器产出的“AI 注水”改写成共同体可读、可继承的论证——Buckmaster 为粗糙草稿致歉，正说明这一步无法跳过。高价值研究角色越来越像研究产品经理 + 智能体群指挥 + 形式化审计员，而非孤独的推导者。

8.2 前沿竞争的新赛场：不是聊天分数，而是“真正前沿处谁被依赖”

• 两条路线都重度依赖 Anthropic Claude 与 OpenAI Codex / GPT-5.6 Sol / GPT-6 Astra，外加 OpenAI 未发布的下一代模型。在最难的智能体长程任务——多文件、长链条、持续自我验证——上，研究者用脚投票真正选了哪些工具，比任何聊天基准都更说明问题。
• 这一事件重新命名的决定性能力轴：长程智能体稳定性、大规模多智能体编排、与形式化/代码工具的协同、产出的可验证性，以及模型代际迭代速度（OpenAI 刻意点出一款“显著强于 GPT-6 Astra、仍在训练”的内部模型——既是能力预告，也是商业信号）。
• 对模型选型：除静态分数外，还要评估长程任务完成度、工具/验证链协同，以及可控、可审计的产出。同时清醒认识到：顶级研究能力，与企业能买到的商用模型之间，隔着一个代际与一次发布滞后。

8.3 一台资本密集的科学仪器——尚非廉价 API 能力

数百万美元、约一万并发智能体、约 1300 亿输出 token、88 小时，再加一款你买不到的未发布模型：这更像在粒子对撞机上跑实验，而非调用 API。它短期内不会成为中小企业用得起的标准服务。最先、也远更确定被产品化的，是流水线被拆解后的部件：形式验证工具、代码/研究智能体编排框架、可审计的研究协作环境，以及垂直的“多智能体搜索 + 验证”工作流。

8.4 规则真空：署名、数据与可复现规范落后于能力

• 作者与功劳：功劳如何在模型、造模型的公司、驾驭智能体的研究者，以及开辟路线的人之间分配？当参与者效力于竞争对手时，联合发布又如何可能？
• 数据边界：厂商能否、以及在何种退出设置下，可用喂入其工具的未发表成果改进模型，这需要比现状清晰得多的默认规则与技术保障。
• 可复现性：当关键结果依赖未发布模型，共同体如何独立重复？“公开产物 + 黑箱过程”足以构成一项发现吗？
• 评价体系：当机器核验证明成为常态，同行评审、期刊、招聘与奖项都要被重新设计。

这些都不会因这一次事件而定论，但它像一次压力测试，提前把账单递到了整个学术与产业系统面前。

2026 年 9 月第一周，真正跨过门槛的不是“AI 解决了一道千禧年难题”这个结果，而是生产方式本身——大规模并行智能体搜索、以形式化验证为兜底、由人定义问题——第一次在一道千禧年级别的开放问题上跑通完整闭环。

对数学结果本身，我们建议与学界同样的耐心与不可知：Lean 背书给了它很高的下限，但在独立复现、命题等价性审计、同行评审与两年考验之前，严谨措辞仍是“一份待验证的证明”，克雷页面仍写着未解。优先权与数据之争应交给证据；眼下它至多是两份并排而立的说法。

观察清单（可证伪）

• 独立构建：是否有外部团队成功编译 OpenAI 的 Lean 仓库，并逐行验证其形式化定义与 Fefferman 官方 C/D 等价？
• 专家解读：领域内数学家（Córdoba、Martínez-Zoroa、Silvestre、Tao 等）的公开判断。
• 路线收敛：两人的受迫 Euler / 亚耗散 NS，与 OpenAI 的无外力 Euler / 完整 NS，最终会被证明是同一条路、还是实质不同？
• 在公开模型上复现：这套智能体群攻势能在任何人都能访问的模型（而非 OpenAI 未发布模型）上重跑吗？这决定范式的可迁移性。
• 克雷的立场：“未解”标签是否、何时改变。
• 数据/署名的新证据：邮件、对 Codex 数据条款的权威解读，以及任何能把单方说法变成可核查事实的东西。

给从业者三个更确定的结论：能力信号是真实的——“AI 只会做习题、不会做研究”已经过时；人的角色改变了，却更具决定性——好问题、搜索空间设计、等价性核查与人类可读的洞见才是护城河；面向市场则要拆解并管理预期——完整运行是资本密集的仪器，而验证、编排与审计才是最先产品化的部件，同时应以长程智能体、工具协同与可验证产出来评判模型。