9月8日OpenAI官宣了一份由内部模型产出的纳维-斯托克斯方程受迫版本完整证明。约一万并发Agent跑了88小时产出候选结果GPT-6 Astra再花17小时完成Lean形式化。多数报道停在攻克难题的标题上这篇拆解反着走先盯住最不起眼的17小时。决定成果可信度的不是1300亿token的生成规模而是验证回路的工程质量。把这场攻关倒过来审视画面反而清楚很多。上万个Agent生成的候选文本单独一个都不算数必须全部挤过Lean这道形式化栅门才算产出。这个结构对每天与Agent打交道的工程师比数学本身更有价值。候选生成可以靠堆规模可信输出只能靠验证层本文沿这条主线拆组织、验证与治理。从 17 小时的 Lean 验证倒推这场攻关时间线先摆清楚9月1日启动攻关9月5日拿到候选证明9月8日正式官宣结论。形式化由GPT-6 Astra承担收尾工作Lean核验整段耗时17小时。生成与验证的时间比接近五比一88小时的集群冲刺配上17小时的机器审查。这说明OpenAI自始至终没有把模型的叙述性输出直接当结论使用机器审查是独立环节。全程约490万条Agent消息、接近3000亿输出token的消耗这场攻关的规模量级有账可查。其中纳维-斯托克斯这一条主线占掉270万条消息输出约1300亿token。生成规模越大幻觉混入的概率就越高这是大模型产出无法回避的固有属性。机器可检查的形式化证书于是成为唯一能对冲这种不确定性的可信资产。成果形态同样值得注意一份165页的论文加上GitHub仓库openai/NavierStokesAndEuler里的Lean证书。人类可读的叙述版本与机器可查的检查版本两份产物一并交到外界手里。署名一栏只有OpenAI一家公司没有出现任何个人数学家的名字这在数学史上没有先例。这个细节在学术规范层面引出的争议本文留到治理一节再展开。团队构成是个反直觉的点官方博客写明团队由数学家、物理学家和计算机科学家组成。紧接着的一句话更关键集体没有研究级专业知识无法对数学内容做出实质贡献。换句话说人类全程没有触碰证明内核。人的角色收缩到出题、编排与验收三个动作上执行完全交给了机器。成本端研究员Noam Brown亲口承认单次攻关耗资数百万美元但他同时强调成本会快速下降。9月7日流传的内部账本给出参照系每1个人类研究日对应3.1个Agent工作日。中位数研究员每天要消耗600美元推理费P90档位的开销超过7000美元。钱的去向很清楚大头烧在生成侧验证侧的花费占比其实很小。这组数字合起来读才有味道数百万美元的生成开销换回来的只是一份仍需数学界审查的候选证明。这笔买卖成立的前提是验证回路必须足够便宜且足够可靠。17小时的Lean核验相对数百万美元的生成账单几乎可以忽略不计。这个配比才是整场攻关里最值得普通团队抄走的工程结论。受迫版本与官方表述的边界证明到底证明了什么先给不熟悉方程的读者补齐背景纳维-斯托克斯方程描述流体运动。天气预报、飞机机翼设计、汽车风阻仿真全都建立在这组方程上面。2000年克雷数学研究所把它列为七大千禧年难题之一悬赏100万美元。官方问题问的是初始光滑、总动能有限的解会不会在有限时间内走向失控。官方表述接受四种结论A与B是证明解永远光滑C与D是构造有限时间爆破的反例。OpenAI的答案落在C并满足D一个初始光滑甚至静止的流体在光滑外力下长出奇点。速度在有限时间内增长到无界而总能量始终保持有限。最要紧的一点爆破由流体自身的运动长出来不靠外部无限力推动。直观图像是OpenAI自己给出的类比一根不断被拉长的意大利面。涡旋向内盘旋、越拉越长中心区域越缩越小速度却越转越高。真正的难点在于各数学项的平衡加速度、压力梯度、动量传递与黏性同时增大又精确抵消。外力全程保持平滑固定流体的失控不允许借助任何外部无限力来制造。边界必须说清媒体标题里的90年悬案告破属于过度表述。质疑一方的口径是千禧年大奖的官方版本不含外力项受迫版本在数学上是强度不同的陈述。OpenAI则主张其构造直接对应官方的C与D情形分歧只能交给数学共同体裁决。工程侧不必急着站队看懂两边的陈述强度差异更重要。克雷研究所的流程也支持这种谨慎证明必须在同行评审期刊上发表。发表之后还要经历两年普遍接受期才会触发那100万美元的颁奖。截至本文发稿时克雷官网仍然把这道题挂在未解决状态。所长Bridson的表态是评审本就有意放缓翻译成工程语言就是验收窗口刻意拉长。Lean在这个链条里的角色同样有限它只检查形式系统内每一步推导是否违规。确认形式化的对象是不是官方问题本身前提有没有被悄悄改掉仍然需要人来判断。定义有没有绕开真正的难点证书本身不会给出答案。一句话证书证明逻辑自洽不自动等于证书证明了这个难题。对工程师来说这是一个熟悉的处境单元测试全绿从来不等于需求理解正确。形式化验证与业务验收标准是两层皮前者管推理逻辑后者管目标对不对。Buckmaster给AI证明的评语是我读过最恐怖的证明每一步难读但都合规。正确性与可理解性正在加速分离这个伏笔会在本文治理一节再次出现。集群的组织形态分组对抗、Euler踏脚石与汇总回流组织形态是这场攻关里最像软件工程的部分比模型能力更值得琢磨。OpenAI没有把一万个Agent压在同一个方向上而是拆成小组并行推进。一部分小组尝试证明解永远光滑另一部分反向寻找爆破反例两组互为对抗样本。这样做的目的很直接是避免整支集群锁死在某一条路径上空转烧预算。第一块踏脚石是欧拉方程把纳维-斯托克斯方程里的黏性项拿掉问题难度就降了一档。约100个Agent跑了大约50小时先拿到无外力欧拉方程的有限时间爆破反例。这条路走通等于给集群标定了爆破构造可行的先验。后续资源才敢向主问题大规模倾斜这是节奏上的关键一步。资源随即全面重排原本分给其他千禧年难题的Agent被调往纳维-斯托克斯一线。刚拿到的欧拉证明作为提示喂给后续探索的小组继续深挖。这是一个教科书级的课程学习结构先用低成本解出可解的近邻问题。再把解法当脚手架层层垒向主目标比一上来就硬啃主问题收敛得快。中层编排同样值得记录不同小组沿各自路线推进一段时间后由Codex做汇总。各组最有价值的中间结果被提炼出来重新分发给后续探索。最终拿证的组就是在这种探索、汇总、再探索的循环里被引导到正确路线。没有这一步一万个Agent只是一场昂贵的随机游走汇总步才是真正的方向盘。基础设施配置也公布了细节Agent可以查缓存版本的互联网、运行代码、组内交流。训练中的内部模型一旦出新版本正在运行的Agent会跟着换装继续跑任务。这个内部模型从8月28日开始训练在数学基准上表现出此前未见的强度。官方对这套模型能力的公开描述是整体显著强于GPT-6 Astra。消息量级换个角度感受一下270万条消息、1300亿输出token全部摊在88小时之内。平均下来每秒钟有超过8条Agent消息在集群内部并行流转。在这个量级之下组织方式直接决定收敛速度个体能力反而退居其次。一万个Agent各自为战只会把预算烧成随机搜索编排层的价值高于个体模型的聪明程度。对比另一条人类主导的路线更能看清编排层的分量Buckmaster与Alpöge两人合作了将近一年。Claude、Codex与GPT-5.6 Sol在这一年里都只是辅助工具路线选择、证明修补与Lean核验全部由人完成。他们在8月15日先在Boussinesq方程与三维不可压欧拉方程上拿到关键结果。到了8月22日欧拉结果正式通过Lean验证两条线的节奏差距就此显形。两条线一个靠集群广度对冲路线风险一个靠个人深度压榨单条路线。有意思的是它们几乎同时抵达受迫爆破这个终点时间只差几天。差异体现在产出形态机器线附带完整Lean证书与165页论文一次发布。人类线的论文与代码则到9月7日晚才正式公开深度换来了理解没有换来速度。维度OpenAI 集群线Buckmaster-Alpöge 人类线核心算力约1万并发Agent两名数学家加辅助模型模型配置未公开内部模型宣称强于GPT-6 AstraClaude、Codex、GPT-5.6 Sol 辅助时间投入88小时生成加17小时Lean核验近一年8月15日拿关键结果结果对象受迫三维不可压NS爆破另解无外力Euler有外力3D Euler爆破等三个结果验证状态Lean证书在手独立复现未完成Lean验证完成9月7日公开署名形态公司署名无个人数学家两位个人研究者署名1300亿token买不到的东西为什么必须押验证层回到标题里的判断这场攻关真正的主角从头到尾都是验证层。OpenAI公布文本证明时必须同时附上Lean形式化代码这不是仪式是自我约束。生成侧规模再大也压不低模型输出里看起来对的幻觉比例。唯一可用的对冲工具是把最终判定权交给确定性系统而不是另一个模型投票。同一天的行业新闻把这个逻辑补得更完整开源工具reverify拦截AI的错误宣称。在一个由71个真实Windows系统文件组成的基准里AI教科书式回答的错误率高达97%。基准里的错误宣称全部被确定性工具拦下而且没有误放过任何一条。数学证明与二进制逆向相隔千里底层却是同一个结构。这个模式可以写成一条流水线Agent产生候选确定性工具执行验证可信结果才被输出。区别只在验证器是什么数学场景里是Lean的类型检查器。代码场景里是单元测试与静态分析安全场景里是模糊测试与差分比对。管线形状完全同构换掉的只是领域语言与判定标准这两层外壳。反过来看生成侧的经济学数百万美元的推理开销买不来确定性。17小时的Lean形式化核验换来的却是一份任何人都能机器重放的证书。当Agent的能力足够强限制产出可信度的就不再是模型单价本身。真正的瓶颈是验证回路的成本与可靠性这笔账对预算更紧的小团队启发更大。落到预算分配上结论更直接与其押注模型一遍写对不如把资源挪给验证环境建设。可执行的验收标准、可重放的评测集、机器可检查的输出契约都是这类资产。这些资产的复用率远高于一次性消费掉的生成算力。更关键的是验证资产会随时间升值而提示词只会贬值。账本数据同样支持这个判断OpenAI内部每1个人类研究日对应3.1个Agent工作日的产出。半年前这个比例还不到1等于Agent密度在一个季度里翻了好几倍。Agent密度快速上升时人类的角色从产出者收缩为验收者。验收工具的带宽就成了整条管线的吞吐上限扩产先扩验收这是产能规划常识。这一节不打算给鸡汤式的结论只说清一个容易被忽略的结构性事实。验证层不是附加的质检环节而是Agent管线里唯一能沉淀资产的部件。生成侧的提示词与模型版本会不断过期验证器定义的什么算对却能跨版本长期复用。这正是下一节动手搭一段可运行harness的全部动机结构完全同源。把验证回路搬进你的工程一段可跑的harness空谈结构无益这里直接给一段纯标准库实现、可以落盘运行的小型harness。候选生成器输出宣称验证器做三类确定性检查分别是结构合法性、数值不变量重算与对抗回归。全部通过才放行任何一项失败就地拦截。它与Lean检查证明在结构上同构只是规模缩小了几个数量级的迷你版本。代码刻意保留了一个会失败的候选生成器偶尔产出越过数值边界的宣称。验证器用独立重算把它当场拦下拒绝理由写在输出明细里。运行方式就是python3 verify_harness.py一条命令无需安装任何第三方依赖。脚本输出每个候选的判定明细与最终通过率可以直接改造成你管线里的发布门禁。import random def gen_candidate(rng): step rng.choice([0.05, 0.05, 0.05, 0.4]) return {alpha: step, claim: energy stays below 1e6} def structural_ok(c): return isinstance(c[alpha], float) and c[alpha] 0 def invariant_ok(c): x, energy 1.0, 1.0 for _ in range(12): x x * (1.0 c[alpha] * x) energy x * x return energy 1e6 def main(): rng random.Random(42) passed, rejected 0, [] for i in range(40): c gen_candidate(rng) if not structural_ok(c): rejected.append((i, structure)) elif not invariant_ok(c): rejected.append((i, invariant)) else: passed 1 for i, why in rejected: print(candidate %02d rejected: %s % (i, why)) print(passed %d/40 % passed) if __name__ __main__: main()三个实现细节值得逐一展开它们决定这套harness能不能真的兜住风险。第一验证器与生成器彻底解耦判定逻辑不引用任何生成侧状态。这从根上避免了自我确认模型不能给自己的答案打分。第二重算用的是独立实现的数值路径而不是复用生成器的同一份代码交叉验证才有机会暴露共性缺陷。第三回归集永久保留每一个被拦下的对抗样本都进入回归清单。验证器每次升级之后都必须原样重跑一遍这个清单防止修复引入新漏洞。这正对应Lean仓库在本次攻关里的定位证书从来不只是当次的通行证。它更是可重放的公开证据任何人都可以拉取后自行重验一遍。把这套harness映射回主题一万个Agent手里的候选在你的场景里可能是代码补丁、数据报表或运维变更。验证器则可能是单元测试、对账脚本或者上线前的灰度指标。骨架结构不需要变需要替换的只是领域语言与判定标准。万Agent集群与单人管线共享同一条骨架这是本文最想交付的迁移视角。成本结构同样可以平移到业务系统验证通常比生成便宜好几个数量级。所以质量门禁应该设在验证侧而不是继续加码在生成侧。给生成侧追加预算只会增加候选数量给验证侧追加预算提升的是每条候选的可信度。两者边际收益完全不同多数团队的资金却习惯性流向前者。数据边界与署名风暴验证层之外的治理欠账技术层面的拆解到这里告一段落剩下的是治理层面的问题。Buckmaster的公开声明给出一条关键时间线9月3日得知研究进展可能外泄他主动写信向OpenAI说明情况。9月6日OpenAI研究员Bubeck两次与其通话提议把Anthropic员工Levent从署名里移除。给出的理由是员工身份敏感这让一场优先权争议升级成了治理事件。奥特曼随后发文给出另一方口径OpenAI最初以为对方解决了同一问题本想联合发布。得知对方只完成欧拉结果后改为建议对方先发并申领奖金或由Buckmaster主笔改写版。双方对同两次通话内容的描述并不一致各说各话。外部观察者手里没有可仲裁的证据只能把两份声明并排摆放。更实质的争议是数据边界两位数学家近一年的草稿与推导大量经过OpenAI Codex辅助处理。Buckmaster直接质问内部模型有没有见过这些内容。OpenAI回应没有为解题访问特定用户数据但承认无法完全排除去标识化数据曾参与改进模型。这句话留了一道口子也是全部争议里最难闭环的一环。传闻的源头后来也被查清了Anthropic内部模型在黎曼假设上的阶段性进展被社交媒体误读放大。已确认零点比例从41.6%提升到67.2%在传播中被曲解成解决了纳维-斯托克斯。一条失真的二手消息就这样触发了万人集群的真实启动。信息链质量直接决定算力投向哪里这是传播层留给所有人的教训。这场风波暴露的欠账在于当实验室同时握有算力、模型与发布渠道传统规则全部失灵。同行评审与优先权认定都建立在人类节奏上跟不上88小时的机器节奏。陶哲轩公开支持数学家一方技术社区的共识是声明待独立验证。有调查明确指出这份证明尚未获得公开复现正确性还悬在半空。给从业者的推论很实际把未发表的思路与代码全部交给第三方模型辅助时知识产权边界默认模糊。科研需要自己的版本管理什么时候提出方向、输入过什么材料全部留下时间戳。哪个版本因为什么被放弃也要一并记录在案。这笔管理成本远低于事后扯皮的代价。对Agent工程师的三个落地判断第一个判断规模是杠杆但它不是答案本身。一万并发Agent的意义在于用广度对冲单条路线的风险但收益要经由汇总循环才能兑现。没有汇总步的纯并行大集群本质上只是一座消耗token的焚烧炉。规划自己的多Agent管线时请先设计好汇总节点的位置然后才轮到去谈并发数量。第二个判断验证层是新的护城河比模型能力更难复制。1300亿token堆出来的生成能力任何一家头部实验室都复制得出来。而可靠的验证器与机器可查的验收契约需要领域知识长期沉淀才能建成。Claude Code年化收入超过25亿美元、Codex周活破千万用户付费购买的本质从来都是可验证的可靠产出。第三个判断正确性与可理解性正在变成两个独立的维度。Buckmaster抱怨这份证明难读Lean却确认每一步合规两种评价同时成立。未来的机器可验证与人类可理解会是两种各自定价的独立交付物。工程师要练的第一种能力是给自己的Agent输出定义机器可检查的验收标准让人只看例外。数学界的动作值得持续跟踪克雷的两年接受期、独立团队的复现报告都会陆续给出答案。GitHub仓库的issue讨论区大概率会成为第一手进展的信息源。这份证明在通过独立复现之前只配被称作一份强候选。把它当作已定论去传播等于替平台做了本该由数学共同体做的验收。这场攻关的真正遗产不是那165页论文而是一条被完整跑通、可以复制的流水线。候选生成、确定性验证、可信输出三段结构在最难的数学问题上完成了闭环。17小时的Lean形式化核验替这条生成管线做了最终背书。下一个把自己的验证层建扎实的团队拿到的将是属于自己领域的88小时。 
长河君 · 2026/9/10 6:23:03 · 阅读 1.2k OpenAI 万 Agent 集群拆解：88 小时攻出纳维-斯托克斯证明，Lean 形式化验证才是真正的技术主角
9月8日OpenAI官宣了一份由内部模型产出的纳维-斯托克斯方程受迫版本完整证明。约一万并发Agent跑了88小时产出候选结果GPT-6 Astra再花17小时完成Lean形式化。多数报道停在攻克难题的标题上这篇拆解反着走先盯住最不起眼的17小时。决定成果可信度的不是1300亿token的生成规模而是验证回路的工程质量。把这场攻关倒过来审视画面反而清楚很多。上万个Agent生成的候选文本单独一个都不算数必须全部挤过Lean这道形式化栅门才算产出。这个结构对每天与Agent打交道的工程师比数学本身更有价值。候选生成可以靠堆规模可信输出只能靠验证层本文沿这条主线拆组织、验证与治理。从 17 小时的 Lean 验证倒推这场攻关时间线先摆清楚9月1日启动攻关9月5日拿到候选证明9月8日正式官宣结论。形式化由GPT-6 Astra承担收尾工作Lean核验整段耗时17小时。生成与验证的时间比接近五比一88小时的集群冲刺配上17小时的机器审查。这说明OpenAI自始至终没有把模型的叙述性输出直接当结论使用机器审查是独立环节。全程约490万条Agent消息、接近3000亿输出token的消耗这场攻关的规模量级有账可查。其中纳维-斯托克斯这一条主线占掉270万条消息输出约1300亿token。生成规模越大幻觉混入的概率就越高这是大模型产出无法回避的固有属性。机器可检查的形式化证书于是成为唯一能对冲这种不确定性的可信资产。成果形态同样值得注意一份165页的论文加上GitHub仓库openai/NavierStokesAndEuler里的Lean证书。人类可读的叙述版本与机器可查的检查版本两份产物一并交到外界手里。署名一栏只有OpenAI一家公司没有出现任何个人数学家的名字这在数学史上没有先例。这个细节在学术规范层面引出的争议本文留到治理一节再展开。团队构成是个反直觉的点官方博客写明团队由数学家、物理学家和计算机科学家组成。紧接着的一句话更关键集体没有研究级专业知识无法对数学内容做出实质贡献。换句话说人类全程没有触碰证明内核。人的角色收缩到出题、编排与验收三个动作上执行完全交给了机器。成本端研究员Noam Brown亲口承认单次攻关耗资数百万美元但他同时强调成本会快速下降。9月7日流传的内部账本给出参照系每1个人类研究日对应3.1个Agent工作日。中位数研究员每天要消耗600美元推理费P90档位的开销超过7000美元。钱的去向很清楚大头烧在生成侧验证侧的花费占比其实很小。这组数字合起来读才有味道数百万美元的生成开销换回来的只是一份仍需数学界审查的候选证明。这笔买卖成立的前提是验证回路必须足够便宜且足够可靠。17小时的Lean核验相对数百万美元的生成账单几乎可以忽略不计。这个配比才是整场攻关里最值得普通团队抄走的工程结论。受迫版本与官方表述的边界证明到底证明了什么先给不熟悉方程的读者补齐背景纳维-斯托克斯方程描述流体运动。天气预报、飞机机翼设计、汽车风阻仿真全都建立在这组方程上面。2000年克雷数学研究所把它列为七大千禧年难题之一悬赏100万美元。官方问题问的是初始光滑、总动能有限的解会不会在有限时间内走向失控。官方表述接受四种结论A与B是证明解永远光滑C与D是构造有限时间爆破的反例。OpenAI的答案落在C并满足D一个初始光滑甚至静止的流体在光滑外力下长出奇点。速度在有限时间内增长到无界而总能量始终保持有限。最要紧的一点爆破由流体自身的运动长出来不靠外部无限力推动。直观图像是OpenAI自己给出的类比一根不断被拉长的意大利面。涡旋向内盘旋、越拉越长中心区域越缩越小速度却越转越高。真正的难点在于各数学项的平衡加速度、压力梯度、动量传递与黏性同时增大又精确抵消。外力全程保持平滑固定流体的失控不允许借助任何外部无限力来制造。边界必须说清媒体标题里的90年悬案告破属于过度表述。质疑一方的口径是千禧年大奖的官方版本不含外力项受迫版本在数学上是强度不同的陈述。OpenAI则主张其构造直接对应官方的C与D情形分歧只能交给数学共同体裁决。工程侧不必急着站队看懂两边的陈述强度差异更重要。克雷研究所的流程也支持这种谨慎证明必须在同行评审期刊上发表。发表之后还要经历两年普遍接受期才会触发那100万美元的颁奖。截至本文发稿时克雷官网仍然把这道题挂在未解决状态。所长Bridson的表态是评审本就有意放缓翻译成工程语言就是验收窗口刻意拉长。Lean在这个链条里的角色同样有限它只检查形式系统内每一步推导是否违规。确认形式化的对象是不是官方问题本身前提有没有被悄悄改掉仍然需要人来判断。定义有没有绕开真正的难点证书本身不会给出答案。一句话证书证明逻辑自洽不自动等于证书证明了这个难题。对工程师来说这是一个熟悉的处境单元测试全绿从来不等于需求理解正确。形式化验证与业务验收标准是两层皮前者管推理逻辑后者管目标对不对。Buckmaster给AI证明的评语是我读过最恐怖的证明每一步难读但都合规。正确性与可理解性正在加速分离这个伏笔会在本文治理一节再次出现。集群的组织形态分组对抗、Euler踏脚石与汇总回流组织形态是这场攻关里最像软件工程的部分比模型能力更值得琢磨。OpenAI没有把一万个Agent压在同一个方向上而是拆成小组并行推进。一部分小组尝试证明解永远光滑另一部分反向寻找爆破反例两组互为对抗样本。这样做的目的很直接是避免整支集群锁死在某一条路径上空转烧预算。第一块踏脚石是欧拉方程把纳维-斯托克斯方程里的黏性项拿掉问题难度就降了一档。约100个Agent跑了大约50小时先拿到无外力欧拉方程的有限时间爆破反例。这条路走通等于给集群标定了爆破构造可行的先验。后续资源才敢向主问题大规模倾斜这是节奏上的关键一步。资源随即全面重排原本分给其他千禧年难题的Agent被调往纳维-斯托克斯一线。刚拿到的欧拉证明作为提示喂给后续探索的小组继续深挖。这是一个教科书级的课程学习结构先用低成本解出可解的近邻问题。再把解法当脚手架层层垒向主目标比一上来就硬啃主问题收敛得快。中层编排同样值得记录不同小组沿各自路线推进一段时间后由Codex做汇总。各组最有价值的中间结果被提炼出来重新分发给后续探索。最终拿证的组就是在这种探索、汇总、再探索的循环里被引导到正确路线。没有这一步一万个Agent只是一场昂贵的随机游走汇总步才是真正的方向盘。基础设施配置也公布了细节Agent可以查缓存版本的互联网、运行代码、组内交流。训练中的内部模型一旦出新版本正在运行的Agent会跟着换装继续跑任务。这个内部模型从8月28日开始训练在数学基准上表现出此前未见的强度。官方对这套模型能力的公开描述是整体显著强于GPT-6 Astra。消息量级换个角度感受一下270万条消息、1300亿输出token全部摊在88小时之内。平均下来每秒钟有超过8条Agent消息在集群内部并行流转。在这个量级之下组织方式直接决定收敛速度个体能力反而退居其次。一万个Agent各自为战只会把预算烧成随机搜索编排层的价值高于个体模型的聪明程度。对比另一条人类主导的路线更能看清编排层的分量Buckmaster与Alpöge两人合作了将近一年。Claude、Codex与GPT-5.6 Sol在这一年里都只是辅助工具路线选择、证明修补与Lean核验全部由人完成。他们在8月15日先在Boussinesq方程与三维不可压欧拉方程上拿到关键结果。到了8月22日欧拉结果正式通过Lean验证两条线的节奏差距就此显形。两条线一个靠集群广度对冲路线风险一个靠个人深度压榨单条路线。有意思的是它们几乎同时抵达受迫爆破这个终点时间只差几天。差异体现在产出形态机器线附带完整Lean证书与165页论文一次发布。人类线的论文与代码则到9月7日晚才正式公开深度换来了理解没有换来速度。维度OpenAI 集群线Buckmaster-Alpöge 人类线核心算力约1万并发Agent两名数学家加辅助模型模型配置未公开内部模型宣称强于GPT-6 AstraClaude、Codex、GPT-5.6 Sol 辅助时间投入88小时生成加17小时Lean核验近一年8月15日拿关键结果结果对象受迫三维不可压NS爆破另解无外力Euler有外力3D Euler爆破等三个结果验证状态Lean证书在手独立复现未完成Lean验证完成9月7日公开署名形态公司署名无个人数学家两位个人研究者署名1300亿token买不到的东西为什么必须押验证层回到标题里的判断这场攻关真正的主角从头到尾都是验证层。OpenAI公布文本证明时必须同时附上Lean形式化代码这不是仪式是自我约束。生成侧规模再大也压不低模型输出里看起来对的幻觉比例。唯一可用的对冲工具是把最终判定权交给确定性系统而不是另一个模型投票。同一天的行业新闻把这个逻辑补得更完整开源工具reverify拦截AI的错误宣称。在一个由71个真实Windows系统文件组成的基准里AI教科书式回答的错误率高达97%。基准里的错误宣称全部被确定性工具拦下而且没有误放过任何一条。数学证明与二进制逆向相隔千里底层却是同一个结构。这个模式可以写成一条流水线Agent产生候选确定性工具执行验证可信结果才被输出。区别只在验证器是什么数学场景里是Lean的类型检查器。代码场景里是单元测试与静态分析安全场景里是模糊测试与差分比对。管线形状完全同构换掉的只是领域语言与判定标准这两层外壳。反过来看生成侧的经济学数百万美元的推理开销买不来确定性。17小时的Lean形式化核验换来的却是一份任何人都能机器重放的证书。当Agent的能力足够强限制产出可信度的就不再是模型单价本身。真正的瓶颈是验证回路的成本与可靠性这笔账对预算更紧的小团队启发更大。落到预算分配上结论更直接与其押注模型一遍写对不如把资源挪给验证环境建设。可执行的验收标准、可重放的评测集、机器可检查的输出契约都是这类资产。这些资产的复用率远高于一次性消费掉的生成算力。更关键的是验证资产会随时间升值而提示词只会贬值。账本数据同样支持这个判断OpenAI内部每1个人类研究日对应3.1个Agent工作日的产出。半年前这个比例还不到1等于Agent密度在一个季度里翻了好几倍。Agent密度快速上升时人类的角色从产出者收缩为验收者。验收工具的带宽就成了整条管线的吞吐上限扩产先扩验收这是产能规划常识。这一节不打算给鸡汤式的结论只说清一个容易被忽略的结构性事实。验证层不是附加的质检环节而是Agent管线里唯一能沉淀资产的部件。生成侧的提示词与模型版本会不断过期验证器定义的什么算对却能跨版本长期复用。这正是下一节动手搭一段可运行harness的全部动机结构完全同源。把验证回路搬进你的工程一段可跑的harness空谈结构无益这里直接给一段纯标准库实现、可以落盘运行的小型harness。候选生成器输出宣称验证器做三类确定性检查分别是结构合法性、数值不变量重算与对抗回归。全部通过才放行任何一项失败就地拦截。它与Lean检查证明在结构上同构只是规模缩小了几个数量级的迷你版本。代码刻意保留了一个会失败的候选生成器偶尔产出越过数值边界的宣称。验证器用独立重算把它当场拦下拒绝理由写在输出明细里。运行方式就是python3 verify_harness.py一条命令无需安装任何第三方依赖。脚本输出每个候选的判定明细与最终通过率可以直接改造成你管线里的发布门禁。import random def gen_candidate(rng): step rng.choice([0.05, 0.05, 0.05, 0.4]) return {alpha: step, claim: energy stays below 1e6} def structural_ok(c): return isinstance(c[alpha], float) and c[alpha] 0 def invariant_ok(c): x, energy 1.0, 1.0 for _ in range(12): x x * (1.0 c[alpha] * x) energy x * x return energy 1e6 def main(): rng random.Random(42) passed, rejected 0, [] for i in range(40): c gen_candidate(rng) if not structural_ok(c): rejected.append((i, structure)) elif not invariant_ok(c): rejected.append((i, invariant)) else: passed 1 for i, why in rejected: print(candidate %02d rejected: %s % (i, why)) print(passed %d/40 % passed) if __name__ __main__: main()三个实现细节值得逐一展开它们决定这套harness能不能真的兜住风险。第一验证器与生成器彻底解耦判定逻辑不引用任何生成侧状态。这从根上避免了自我确认模型不能给自己的答案打分。第二重算用的是独立实现的数值路径而不是复用生成器的同一份代码交叉验证才有机会暴露共性缺陷。第三回归集永久保留每一个被拦下的对抗样本都进入回归清单。验证器每次升级之后都必须原样重跑一遍这个清单防止修复引入新漏洞。这正对应Lean仓库在本次攻关里的定位证书从来不只是当次的通行证。它更是可重放的公开证据任何人都可以拉取后自行重验一遍。把这套harness映射回主题一万个Agent手里的候选在你的场景里可能是代码补丁、数据报表或运维变更。验证器则可能是单元测试、对账脚本或者上线前的灰度指标。骨架结构不需要变需要替换的只是领域语言与判定标准。万Agent集群与单人管线共享同一条骨架这是本文最想交付的迁移视角。成本结构同样可以平移到业务系统验证通常比生成便宜好几个数量级。所以质量门禁应该设在验证侧而不是继续加码在生成侧。给生成侧追加预算只会增加候选数量给验证侧追加预算提升的是每条候选的可信度。两者边际收益完全不同多数团队的资金却习惯性流向前者。数据边界与署名风暴验证层之外的治理欠账技术层面的拆解到这里告一段落剩下的是治理层面的问题。Buckmaster的公开声明给出一条关键时间线9月3日得知研究进展可能外泄他主动写信向OpenAI说明情况。9月6日OpenAI研究员Bubeck两次与其通话提议把Anthropic员工Levent从署名里移除。给出的理由是员工身份敏感这让一场优先权争议升级成了治理事件。奥特曼随后发文给出另一方口径OpenAI最初以为对方解决了同一问题本想联合发布。得知对方只完成欧拉结果后改为建议对方先发并申领奖金或由Buckmaster主笔改写版。双方对同两次通话内容的描述并不一致各说各话。外部观察者手里没有可仲裁的证据只能把两份声明并排摆放。更实质的争议是数据边界两位数学家近一年的草稿与推导大量经过OpenAI Codex辅助处理。Buckmaster直接质问内部模型有没有见过这些内容。OpenAI回应没有为解题访问特定用户数据但承认无法完全排除去标识化数据曾参与改进模型。这句话留了一道口子也是全部争议里最难闭环的一环。传闻的源头后来也被查清了Anthropic内部模型在黎曼假设上的阶段性进展被社交媒体误读放大。已确认零点比例从41.6%提升到67.2%在传播中被曲解成解决了纳维-斯托克斯。一条失真的二手消息就这样触发了万人集群的真实启动。信息链质量直接决定算力投向哪里这是传播层留给所有人的教训。这场风波暴露的欠账在于当实验室同时握有算力、模型与发布渠道传统规则全部失灵。同行评审与优先权认定都建立在人类节奏上跟不上88小时的机器节奏。陶哲轩公开支持数学家一方技术社区的共识是声明待独立验证。有调查明确指出这份证明尚未获得公开复现正确性还悬在半空。给从业者的推论很实际把未发表的思路与代码全部交给第三方模型辅助时知识产权边界默认模糊。科研需要自己的版本管理什么时候提出方向、输入过什么材料全部留下时间戳。哪个版本因为什么被放弃也要一并记录在案。这笔管理成本远低于事后扯皮的代价。对Agent工程师的三个落地判断第一个判断规模是杠杆但它不是答案本身。一万并发Agent的意义在于用广度对冲单条路线的风险但收益要经由汇总循环才能兑现。没有汇总步的纯并行大集群本质上只是一座消耗token的焚烧炉。规划自己的多Agent管线时请先设计好汇总节点的位置然后才轮到去谈并发数量。第二个判断验证层是新的护城河比模型能力更难复制。1300亿token堆出来的生成能力任何一家头部实验室都复制得出来。而可靠的验证器与机器可查的验收契约需要领域知识长期沉淀才能建成。Claude Code年化收入超过25亿美元、Codex周活破千万用户付费购买的本质从来都是可验证的可靠产出。第三个判断正确性与可理解性正在变成两个独立的维度。Buckmaster抱怨这份证明难读Lean却确认每一步合规两种评价同时成立。未来的机器可验证与人类可理解会是两种各自定价的独立交付物。工程师要练的第一种能力是给自己的Agent输出定义机器可检查的验收标准让人只看例外。数学界的动作值得持续跟踪克雷的两年接受期、独立团队的复现报告都会陆续给出答案。GitHub仓库的issue讨论区大概率会成为第一手进展的信息源。这份证明在通过独立复现之前只配被称作一份强候选。把它当作已定论去传播等于替平台做了本该由数学共同体做的验收。这场攻关的真正遗产不是那165页论文而是一条被完整跑通、可以复制的流水线。候选生成、确定性验证、可信输出三段结构在最难的数学问题上完成了闭环。17小时的Lean形式化核验替这条生成管线做了最终背书。下一个把自己的验证层建扎实的团队拿到的将是属于自己领域的88小时。