数学史上大概没有哪个证明处在如此荒诞的位置：它的正确性第一次无可争议——Lean 形式化验证摆在那里，任何怀疑者都可以让证明助手内核逐行重跑一遍；但围绕它的归属争议却比近百年任何数学成果都喧嚣——谁先做出来的、模型是不是吃了用户的数据、一家公司有没有资格「独立」解决同一个问题，每一个问题都没有答案。
9 月 8 日，OpenAI 发布了 Navier-Stokes 存在性与光滑性问题的解：初始光滑、处于静止的三维不可压流体，在光滑外力作用下可以在有限时间内发展出奇点。这个 2000 年被 Clay 研究所列为千禧年七大难题、悬置约 90 年的问题，由约一万个并发 AI Agent 协作 88 小时给出证明，随后 17 小时完成 Lean 形式化。同一周，NYU 教授 Tristan Buckmaster 公开指控 OpenAI 在此过程中施压、要求他撤掉论文里的 Anthropic 合作者。
把这两件事放在一起看，会发现一个比「AI 解决千禧年难题」深刻得多的命题：机器验证解决了「对不对」，却让「信不信」第一次失去了着落。
一场 88 小时的冲刺，和一次措手不及的泄露
先还原时间线，细节全部来自双方公开声明。
Buckmaster 与合作者 Levent Alpöge（Anthropic 员工）用 Claude 和 OpenAI 的 Codex（跑 GPT-5.6 Sol）工作了数月，8 月中旬取得多项突破，包括 forced Euler 方程的爆破结果和一个尚未发表、未形式化验证的 Navier-Stokes 变体。他们的路线建立在两位西班牙数学家 Córdoba 与 Martínez 的构造之上——一条冷门到「几乎没人在走」的路。
9 月初，关于「有人用 AI 做出了千禧年难题级别突破」的传闻开始流传，并且传进了 OpenAI。9 月 1 日，OpenAI 启动对全部开放千禧年难题的评估。9 月 3 日，Buckmaster 主动联系 OpenAI 的一位数学家澄清：这是纯个人合作，与任何机构无关。OpenAI 当天回复、索要细节、提出提供算力。随后节奏骤然加快：周五要求当天通话，周日中午 12:45 问「今天任何时候有空吗」。周日，OpenAI 的 Sébastien Bubeck 加入，两通电话里告知：内部模型产出了约 100 页的 forced Navier-Stokes 证明。
而 OpenAI 那边的完整版本是：8 月 28 日开始训练一个数学能力前所未见的内部模型（「显著强于 GPT-6 Astra」，且性能仍在爬坡）；9 月 1 日听到传闻后，把 Agent 集群撒向所有千禧年难题——先是约 100 个 Agent 花了 50 小时意外解决了 unforced Euler 正则性问题，随后全军转向 Navier-Stokes；9 月 5 日拿到解，9 月 6 日完成 Lean 验证。整个过程 Agent 发送 270 万条消息、消耗约 1300 亿输出 token，研究负责人 Mark Chen 透露仅算力成本就达数百万美元。
两条线在 9 月 6 日交汇：OpenAI 完成验证后联系 Buckmaster，提议「共同发布并承认你们的优先权」——这时才发现对方解的是 forced Euler，不是 Navier-Stokes。而在此之前，Bubeck 被指在两通电话中两次要求把 Alpöge 从作者名单里去掉，理由是他在 Anthropic 任职这件事「太烦人了」。当 Buckmaster 表示将公开此事时，据其声明，得到的回应是「你为什么要毁掉自己的职业生涯」，以及那句后来被反复引用的：「如果我不想客气，我就不必客气。」
OpenAI 的官方否认很完整：研究者和 Agent 从未通过任何途径见过对方的工作，没有访问任何特定用户数据；但也留了一句要命的话——「虽然可能性不大，我们不能排除他们的产品使用产生的去标识化数据帮助改进了我们的模型。」
Buckmaster 在 Mastodon 上的回应一针见血：「他们公开承认使用了我们得出结果之后这段时间的训练数据。用客户的数据去抢客户的研究，这合乎伦理吗？」
机器验证终结了「对不对」的争论
先说这件事光明的一面，因为它被争议掩盖了，但其实是真正的历史分水岭。
Navier-Stokes 证明的交付物不是一个 PDF，而是一份 Lean 形式化代码。这意味着它的正确性检查从「请几十位流体力学专家审读两年」压缩为「在一台笔记本上跑一次证明内核」。Lean 的内核极小且经过多重独立实现验证，它不关心作者的声誉、机构的背景、论文发在哪个期刊。陶哲轩过去几年反复示范过这条路线；这次 OpenAI 用 17 小时把它自动化了。
这对数学意味着什么？Perelman 证明庞加莱猜想后，验证工作由三个独立小组花了数年才完成。而这次的验证成本趋近于零。数学共同体运行了几百年的社会信任机制——同行评审、专家共识、长期复现——在这类问题上已经被机械信任取代。这不是坏事，恰恰是 Agent 科研能够成立的前提：一万个 Agent 跑 88 小时产出的东西，人类专家根本审不过来，只有机器能审。
但注意一个微妙的错位：机器验证覆盖的只有「证明内部」的正确性。证明之外的整个世界——谁想到的思路、谁先完成、模型是否借鉴了某人的草稿——机器一概不管，而这些恰恰是科学的社会契约真正运行的部分。
「谁先做出来的」第一次没了答案
数学界处理优先权冲突的机制其实很古老也很有效：arXiv 时间戳、期刊投稿记录、会议报告、同行之间的口碑链。微积分归牛顿和莱布尼茨吵了两百年，但至少双方的草稿都是可考证的物理实体。
现在的局面是结构性的新问题，有三个。
第一，训练数据成了不可审计的黑箱。 Buckmaster 团队几个月里把所有草稿都放在 Codex 会话里。OpenAI 说「没有访问任何特定用户数据」——注意措辞，这是说推理时没有查询；而「不能排除去标识化数据帮助改进了模型」说的是训练时。这两个声明完全兼容：你的草稿不需要被「查出来」，只需要在下一版模型的梯度里留下统计指纹。Buckmaster 问过训练的事，据他说，没有收到回答。问题在于这个问题原则上就无法回答——连 OpenAI 自己都无法反向审计某个能力是从哪批数据来的。这是深度学习范式的认识论限制，不是任何一家的道德瑕疵。
第二，工具厂商和科研竞争者的身份合一了。 Buckmaster 用 Codex 做研究，OpenAI 用自家内部模型在同一个问题上冲刺，还能听到关于他工作的传闻。哪怕把所有已知的善意解释都算上——独立产出、时间线成立、证明路径不同——利益冲突仍然是结构性的：你在对手的算力上打磨枪械，枪械的每一发子弹都在帮对手校准。这对所有用前沿闭源模型做敏感研究的人都是一个警告：你的每一次会话都是单向透明的。
第三，「内部模型」绕开了全部公共可验证性。 这次解题的模型不公开、不可复现、基准不可跑，外界对它的全部认知来自 OpenAI 的一篇博客。科研共同体第一次要为一个完全不可审计的系统挂上「解决千禧年难题」的认定。OpenAI 甚至直接宣布不领百万美元奖金——Clay 研究所的规则要求期刊发表加两年评审期，这个流程本来就是为人类数学家设计的，而 OpenAI 的目的也根本不是奖金，是「向世界报告 AI 进展的速度」。学术制度的激励结构对这类玩家完全失效。
三条叠加的结果：正确性有了机器担保，归属却回到了前现代——谁嗓门大、谁发布快、谁的声明稿写得周全，谁就占住叙事。
科研的工业化：传闻即动员令
再看 Agent 集群这件事本身，方法论信息量极大，值得逐条拆。
- 并行变体扫描：不同 Agent 组拿不同的问题变体——A/B 变体（证明方向）和 C/D 变体（否定方向）分给不同组。不押注单一猜想，把「猜哪个方向对」变成并行分支。
- 踏脚石策略：先解一族「更容易」的问题，其中 unforced Euler 正则性被意外解决，随后这个结果被直接注入 Navier-Stokes 方向的 Agent 组作为提示。
- 跨组授粉：用 Codex 把各组最有用的中间洞察 Consolidate 成新的提示，回灌给其他组。注意这一步本身就是 LLM 在做科研管理——不是人。
- 紧急产能调配：听到传闻后把其他千禧年难题上的 Agent 抽调过来，all-in 一个问题。
这套东西的名字不叫「研究」，叫「生产线」。传闻是动员令，算力是产能，88 小时是交付周期。而且这条生产线只在封闭实验室里可能：内部模型领先公开 API 若干个月、可以随时升级到「进一步训练后的版本」、不承受任何外部复现压力。Buckmaster 们用数月走完的路，被一条能紧急扩产的流水线用四天追平——不是能力差距，是生产方式的差距。
成本曲线的另一头是制度真空
OpenAI 的 Noam Brown 给出了一条值得所有技术决策者抄录的曲线：o3 在 ARC-AGI 上达到 87.5% 时花费约 50 万美元，今天同等能力约 20 美元；2025 年数学奥赛金牌水平还是 OpenAI 和 DeepMind 的算力豪赌，2026 年 20 美元的 ChatGPT 订阅就能打平。他的原话：「我相信一年后，每个人的指尖都会有能解决这个量级问题的 AI。」
这次 Navier-Stokes 证明的成本是数百万美元。按这条曲线外推，这类能力进入三位数美元成本区间可能只需两三年。能力在指数下降，制度纹丝不动：优先权认定、署名规范、评审周期、奖金规则，全部还是人类节奏。真空就是这样形成的——当「解决千禧年难题」变成一项订阅服务，而学术共同体连「AI 参与的证明该如何署名」都还没吵出共识。
接下来会发生什么
几个可检验的判断：
形式化验证成为 AI 科研的工作量证明。 高影响力的 AI 数学结果将默认附带 Lean/Coq 形式化，没有机器验证的声明不再被严肃对待——就像没有 PoW 的链不会被承认。这次 17 小时的 Lean 化会被未来所有团队视为流程标配而非加分项。
敏感研究会迁移到可审计的环境。 「数据主权」会从合规话题变成科研方法论话题。做真正前沿工作的人会掂量：是把草稿喂给一个和自己赛跑的闭源产品，还是用可自托管的开源模型换掉一点便利性。这次事件是最好的招生广告。
优先权基础设施会出现。 学术界需要为 Agent 时代的节奏重建时间戳机制——可验证的提交日志、甚至零知识证明式的「我持有某结果但不公开」声明。arXiv 是为人类节奏设计的，撑不住了。
内部模型时差成为竞争核心变量。 公开 API 与实验室内部能力的差距既是定价问题，也是（对国家而言的）战略情报问题。选型时把这条时差计入能力预期，会变成工程师的基本功。
尾声
Buckmaster 在声明的结尾说，他本来想谈的根本不是争端，而是另一件事：一个数学家借助语言模型，一个月能走完过去要走很远很远的路。「这是一个 Deep Blue 对卡斯帕罗夫的时刻。」
1997 年之后，人类棋手没有消失，棋类整个的训练体系被重写了。数学大概正站在同一个门口。只是有一个当年不存在的差别：深蓝读不到卡斯帕罗夫的训练对局记录，而这些对局全都存在 IBM 的服务器上，还顺手训练了下一代深蓝。
Navier-Stokes 方程讲的是：光滑连续的流体，会在有限时间内拉出奇点，连续性假设本身会破裂。过去这一周，学术共同体也经历了一次自己的奇点——同行评审、优先权、署名这些运转了几百年的「连续介质」，在 88 小时的 Agent 冲刺面前，被拉出了第一道裂口。
证明可以被形式化。信任不能。