650 个失败想法之后：Claude 多智能体数学研究的编排与验证链拆解

2026 年 8 月 10 日，Anthropic 发布了一篇标题克制的研究文章：《了解更多关于 Claude 数学能力的信息》。 文章的起因是 Anthropic 员工 Jarred Sumner（一名非数学家）给一个未发布的 Claude 研究版本下达了一个他自称「不合理的挑战」：认真尝试证明黎曼猜想。

结果没有悬念——模型没能证明黎曼猜想。 这个自 1859 年提出、挂着百万美元悬赏的千禧年难题依然悬而未决。真正出乎意料的是过程：在第一次尝试生成并测试了 650 个想法全部失败之后，第二次尝试中，模型协调了约 60 个 Claude 子代理，在一天半的时间里运行 2,400 条 shell 命令、编写数百个 Python 脚本，最终把「黎曼ζ函数临界线零点比例」的已知下界从 41.6% 提升到 67.2%。据 Anthropic 官方研究页面，这是数学家数十年间逐步推进到 41.6% 的同一个常数，Anthropic 同时表示不认为 Claude 使用的技术能通向黎曼猜想的完整证明。

本站资讯 news-7636 已覆盖事件本身，本文不复述新闻。 我们关心的是另一组问题：650 个想法为什么会全部失败？第二次尝试改变了什么——是模型变聪明了，还是组织方式变了？一个「看起来正确」的数学结果，要经过多少层检查才能被人类数学家认真对待？这些问题对 AI 工程师的价值，可能超过 67.2% 这个数字本身，因为其中沉淀的多智能体编排与验证模式是可以迁移到代码、安全、科研审计等场景的。

与站内既有内容的边界： 知识库文章 math-ai-research-001 讨论的是 7 月 GPT-5.6 CDC Proof 凸优化突破的 Prompt 方法论，与本文是不同事件、不同机制；本文聚焦子代理编排与验证链，并明确一个前提——黎曼猜想未被证明，67.2% 只是临界线零点比例的渐近下界。

任何讨论都必须从一个区分开始：这个结果与「证明黎曼猜想」之间的距离，比公众想象的要远得多。

黎曼猜想断言：黎曼ζ函数的所有非平凡零点都落在实部为 1/2 的临界线上。而 Claude 推进的是它的一个弱化替身——至少有多大比例的零点必然在临界线上。这是一个「渐近下界」问题：当搜索高度趋于无穷时，临界线上零点的占比下限。据 Kingy AI 的深度解读（二手来源，对官方论文的总结），Claude 论文声称的精确值是至少 67.250% 的非平凡零点既在临界线上又是单零点，而此前无条件纪录是 Pratt、Robles、Zaharescu、Zeindler 在 2020 年证明的略高于 5/12（约 41.666%）——官方页面以 41.6% 与 67.2% 表述这两个数。

三个容易混淆的陈述必须分开：

关键在于：下界提升到 100% 也不自动等于黎曼猜想成立。 一个足够稀疏的例外集合（比如像完全平方数那样密度趋于零的集合）可以始终躲在密度统计之外。这正是 Anthropic 官方明确表示「不认为 Claude 所用技术能通向黎曼猜想证明」的结构性原因：这类方法对零点做总体平均，天然无法排除稀疏例外。

下界推进的历史节奏，是理解这次跳变为何惊人的标尺。 据 Kingy AI 整理的公开里程碑表（二手来源）：

从 1974 年的三分之一到 2020 年的约 41.666%，人类数学家用了 46 年推进约 8 个百分点；而这次单步跳变约 25.6 个百分点。需要强调的是：各里程碑并非同一技术的直接精化，但这条曲线足以解释为什么数学界会认真对待这份手稿。

据官方页面，第一次尝试中 Claude 生成并测试了 650 个想法，没有一个成功。 官方没有逐条解释失败原因，但从结果的形态可以反推这次失败的结构：650 个想法是「广度搜索」，而这个问题的突破口需要的是「纵深施工」。

下界问题不是靠灵感闪现解决的，它是一条长链条。 据官方页面，Claude 最终的成功路径是：把 Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh（下称 B-G-S-T）近年发表的一系列工作，与 Bombieri 2000 年的论文组合起来，找到一条超越现有下界的方法。官方的简短技术说明指出，Claude 构造了一个由 Weil 诱导二次型的函数空间，利用线上零点产生的正定子空间与线外零点产生的负定子空间，写出一个关于二次型秩的不等式，并用一阶、二阶矩信息完成计算——官方评价说，真正关键的一步是「把整个空间连同正负定性一起处理、并允许二次型非对角」的勇气。

这意味着正确路径需要同时满足多个条件： 找到正确的既有文献组合、把不同论文的记号与设定对齐、完成一串环环相扣的代数变形、并在每一步做数值核查。650 个孤立想法中的任何一个，都很难同时承载这些环节。单代理顺序生成的模式，本质上是在用「再生成一个」对抗「需要搭脚手架」的任务。

官方的一个细节值得玩味： Sumner 的输入大多限于鼓励式消息（基本是「继续」「相信自己」的变体），而这「似乎帮助 Claude 克服了它对自己能否取得实质进展的最初怀疑」。据官方脚注，类似的鼓励式提示也用于帮助 Claude 推翻 Jacobian 猜想。这提示了一个容易被工程师忽略的变量：模型对自身任务能力的先验估计（往往从训练语料中学到「开放难题极难被解决」）会真实影响搜索的持续性与深度。失败后的第二次尝试之所以成功，既因为编排方式改变，也因为模型被说服去进行更深的探索。

本站观点：650 次失败不是浪费，它是第二次尝试的搜索先验。问题不在于模型第一次不够聪明，而在于「单线程灵感搜索」与「多代理纵深施工」是两种资源分配策略，而这个任务的回报曲线只奖励后者。

第二次尝试的核心变化是组织方式。 据官方页面，Claude 在一天半里协调了约 60 个子代理，运行 2,400 条 shell 命令、编写数百个 Python 脚本；子代理们针对已知ζ零点做了数千次数值核查，并互相评审彼此的工作。官方脚注给出了罕见的精确分工账本：

这张账本有三个反直觉之处。

第一，30 个探索代理全部失败，但这次「失败」是有效的。 与第一次会话 650 个想法的失败不同，这 30 个代理的失败发生在有核心主线、有验证者拦截的网络里——它们实际上是在为主线排除错误方向、划定可行域。失败的成本被组织吸收了，而不是像第一次那样直接变成终止条件。

第二，验证者（13 个）与想法供给者（13 个）数量相当，与核心开发者（2 个）形成倒金字塔。 这意味着编排者把接近一半的代理预算花在「检查」而非「生产」上。对数学证明这类错误代价极高的任务，这个配比本身就是一种质量策略。

第三，「协调者-专家」结构而非「对等 swarm」。 据官方描述，是一个协调实例向约 60 个子代理分派任务，子代理之间通过互审发生横向联系——这不是 60 个平等节点的群体智能，而是带层级的研究组织。TechCrunch 将其概括为模型在一天半时间里自主协调整个任务，人类员工几乎只负责发送鼓励消息。

从资源口径看，整个探索横跨两次 Claude Code 会话，共消耗约 3,100 万 output tokens（官方口径）。据 Kingy AI（二手）对披露材料的总结，决定性运行的协调阶段横跨约 54 小时、三个日历日，Anthropic 将其密集协调阶段概括为一天半。

这一节用工程师能消化的语言说明证明骨架。 目的不是复现数学（完整技术细节在 Claude 论文与 Anthropic 的简注中），而是让读者理解：为什么这个结果必须依赖既有文献的组合，以及为什么它的形态注定是「下界」而非「判定」。

核心困难是：零点有无穷多个，且线外零点（如果存在）无法被直接定位。 官方简述与 Kingy AI 对论文的解读给出的概念路径是四步：

第一步，Weil 显式公式作为桥梁。 这是一族把「对ζ零点的求和」与「对素数的求和」联系起来的恒等式。选一个合适的测试函数，就能从素数一侧（可计算、可控）读取零点一侧的统计信息。

第二步，压缩成一个有限维 Hermitian 二次型。 零点信息被打包进一个 Gram 矩阵：临界线上的每个零点贡献一个正的秩一块；线外的一对镜像零点贡献一个不定块（一正一负方向）。

第三步，Sylvester 惯性定律让符号可数。 正方向与负方向的个数在坐标变换下不变，因此即使不知道每个零点在哪里，也能分离出「矩阵的秩里有多少必须来自线上零点」。

第四步，一个秩-迹不等式收口。 用矩阵的迹与 Frobenius 范数（二阶矩信息）换算出线上秩的下界；对偶图像下的一阶、二阶矩计算是解析数论的成熟技术。官方特别指出，关键创新是「把整个空间连同正负定性一起处理、允许二次型非对角」——用 Kingy 的话说，Claude 的贡献是在一组成熟的人类数学之间找到了一座新桥，而非凭空造出结果。

B-G-S-T 系列工作的作用是让 Montgomery 1973 年的技术摆脱「假设黎曼猜想成立」的前提，从而可以无条件地支撑下界推进；Bombieri 2000 年的论文提供了另一条关键输入。B-G-S-T 的代表性工作在 arXiv 公开可查（2306.04799、2501.14545，均为官方页面给出的链接）。Claude 把这两条线接在了一起。

对 AI 产出的数学结果，验证不是事后手续，而是结果的一部分。 官方页面披露的流程，实际上构成了一条四层验证链，每一层的失败模式不同，互为冗余。

第一层：AI 自验证（发现阶段内建）。 据官方页面，Claude 在得出结果后主动做了四件事：让不同子代理评审证明、搜寻反例、从 arXiv 下载 54 篇论文确认该结果此前未被做出、以及从零开始独立重证一遍。注意这四件事分别针对四种失败模式：论证错误、结论为假、优先权冲突、证明依赖隐藏漏洞。特别是「下载 54 篇论文查重」——模型在防范的不是自己的计算错误，而是「这个结果可能早已存在」这种研究型失败。

第二层：内部人类核验。 Claude 主动建议由人类数论学家验证其发现。Anthropic 的两位数学家 Levent Alpöge 与 Ralph Furman 研究了 Claude 的工作，理解新结果与既有工作的关系，并为专家撰写了一份简明陈述证明的注释。

第三层：外部专家速审。 Brian Conrey 与 Dan Goldston——该领域的两位专家（Conrey 本人就是 1989 年下界纪录的创造者）——在短时间通知下审阅了论文。官方用词是 examined，即审阅检查，而非完整同行评审。

第四层：形式化验证。 Claude 与另一名员工 Eric Easley 合作产出了该结果的 Lean 形式化，代码公开在 anthropics/zeta-23-lean 仓库，官方页面明确表示这份形式化「通过了标准验证工具对照检查（passes the standard validation tool comparator）」，该工具即 Lean 官方的 comparator。这是链条中唯一一层提供机器级确定性的环节——前三层都是概率性的人类判断，Lean 内核的通过则是二进制结论。

这条链的设计逻辑值得工程师注意： 每一层都不能单独建立信任。AI 自审可能共享同一模型的盲区；人类速审时间有限；Lean 形式化保证的是「形式化对象与陈述一致」，而不保证「这个陈述值得发表」或「形式化忠实于原始直觉」。四层叠加，才让一个未公开模型的产出进入了可被数学界讨论的状态。

本次事件中 Lean 形式化的存在感，比结果本身更能说明 AI 数学研究的演化方向。 据官方页面，Claude 不仅写出了论文，还与人协作把结果形式化为 Lean 代码并通过了标准验证工具对照——这使「验证」从一种学术礼仪变成了可交付的工程产物。

形式化验证与非形式评审的能力边界是互补的：

「形式化忠实性」是这条链上最微妙的缺口。 Lean 内核通过，意味着代码中陈述的定理被证明了；但「这个定理是否就是数学家关心的那个陈述」「定义是否与领域惯例一致」仍需要人类核对。这正是 Alpöge 与 Furman 的注释、Conrey 与 Goldston 的审阅依然不可替代的原因——形式化消灭了推理错误这一类风险，却没有消灭「证非所问」这一类风险。

对工程师的第二点启示是成本结构。 形式化在这个案例中由 AI 主导完成、人类协作——这与传统形式化数学「人类写 Lean 极其缓慢」的瓶颈恰好相反。如果 AI 能廉价地生产形式化证明，那么「先有可验证的形式化、再进入人类评审」可能反过来成为 AI 数学产出的默认提交格式。本站面试题 math-ai-proof-reliability-001 讨论了如何评估 AI 数学证明的可靠性，可作为延伸阅读。

本站观点：四层验证链的真正创新不是任何单一环节，而是把「AI 自审、人类速审、形式化」编排进同一个可复现流程。这个流程比 67.2% 更接近可迁移的方法论资产。

把视角从数学移开，这次实验实际上演示了一套完整的 agent swarm 工程模式。 以下五点可以直接对照到编码、安全研究、数据审计等场景：

1. 协调者-专家层级，而非对等群体。 一个协调实例掌握全局任务分解，子代理只对自己的子任务负责。对等 swarm 在需要全局一致性的任务（证明、系统迁移、审计报告）上会产生大量互相冲突的中间产物。

2. 验证预算与生产预算对等。 60 个子代理中 13 个专职验证、核心生产只有 2 个。错误代价越高的任务，验证者占比应越高。工程对照：代码生成 agent 团队里，review agent 与 test agent 的数量不应少于生成 agent。

3. 允许「有组织的失败」。 30 个探索代理全部失败，但它们的失败为主线划定了可行域。编排者的职责不是消灭失败，而是让失败发生在便宜的位置、并把失败信息回传给主线。

4. 把「查重」作为显式任务。 下载 54 篇论文确认结果未被做出，对应到工程场景就是：agent 在提出方案前应检索既有代码、既有工单、既有文档。重复发明是研究型任务最常见的隐性浪费。

5. 模型的任务先验是可干预变量。 官方两次提到鼓励式提示帮助 Claude 克服自我怀疑（黎曼猜想与 Jacobian 猜想两个案例）。这说明模型对「这件事值不值得深入」有从训练数据习得的先验，而提示层的持续确认可以改变搜索深度。对长时程 agent 任务，「继续」类信号不是玄学，而是搜索预算的调度手段。

最后一节集中列出风险与不确定性，供读者自行调整对结果的信任权重。

第一，完整同行评审尚未完成。 Conrey 与 Goldston 的参与是「短时间通知下的审阅」，不是期刊意义上的同行评审流程。数学界对 AI 产出的态度也并非一致：据 TechCrunch 报道，一批知名数学家今年 6 月签署公开宣言，担忧 AI 可能侵蚀数学界「证明应归属于具体作者并对其正确性负责」的核心价值；菲尔兹奖得主 Gowers 则公开回应，如果定理不再与数学家绑定，也许并不比「恒星不以天文学家命名」更成问题。

第二，复现性存在结构性限制。 产出模型被描述为「未发布的 Claude 研究版本」，没有公开检查点与权重。数学论证与 Lean 代码是公开的，但产生它们的系统不是——据 Kingy AI 的判断，这使得端到端复现不可能，其他模型能否走通同一条路是未知数。

第三，方法本身有明确的天花板。 据 Kingy AI 对论文的解读（二手），手稿罕见地坦承：在现有「带宽一」的对关联信息下，这条路线的极限大约在 0.68185；要把下界推到 70%、80%、90%，需要更宽傅里叶支撑（分别约 1.04、1.26、1.70）的对关联数据——那是新的数学障碍，不是多花一百万 token 能解锁的参数。这也再次印证：67.2% 不是通往黎曼猜想的中途站，而是一条独立路线的高点。

第四，「46 年 8 个百分点」的比较需要谨慎使用。 该说法以 1974 年 Levinson 的三分之一为起点计算，而各历史里程碑并非同一技术的线性精化。它适合说明跳变的罕见程度，不适合解读为「AI 比人类快 N 倍」的通用结论。

第五，背景风险：这不是孤例。 同据 TechCrunch，今年已有多个 Erdős 问题被 AI 模型解决，OpenAI 公布了其内部 Astra 模型证明的十项重要结果，Anthropic 自己还推翻了长期悬置的 Jacobian 猜想（Remio 的流程复盘也将本次事件定性为「自主证明搜索 vs 数学界把可信论证转化为可信知识的慢流程」之间的张力）。AI 数学产出正在批量出现，而数学界的接收流程（评审、署名、责任归属）还没有为这种流量做好准备——这是比单个结果更大的系统性问题。

回到开头的三个读者问题。

多智能体做数学研究怎么编排？ 答案不是「更多 agent」，而是一个带层级的研究组织：1 个协调者、极少数核心开发者、与核心等量的验证者、允许整建制失败的探索层，外加把查重当显式任务的纪律。60 个子代理里真正产出主线论证的只有 2 个——但剩下的 58 个不是浪费，它们是那 2 个代理赖以工作的组织环境。

AI 给出的数学结果如何验证可信？ 靠四层异构验证链：AI 自审（评审、反例、查重、重证）→ 内部数学家核验 → 外部专家速审 → Lean 形式化内核通过。每一层针对不同的失败模式，任何单层都不足以建立信任。形式化消灭推理错误，人类消灭「证非所问」，两者缺一不可。

650 个失败想法之后发生了什么？ 发生的不是模型变聪明，而是搜索策略从「广度采样」切换到「纵深施工 + 组织化验证」。31M output tokens 买到的，与其说是一个定理，不如说是一份关于 agent swarm 如何做研究的完整操作记录——Anthropic 把论文、形式化仓库、过程记录与解释附录一并公开，这在模型演示史上并不常见。

对 AI 工程师，本文的落点很实际： 当你面对一个错误代价高、链条长、需要组合既有成果的任务时，不要加采样次数，去搭编排结构。验证预算至少与生产预算对等，失败要发生在便宜的位置，形式化能上就上。黎曼猜想依然未被证明，但这次实验留下的编排与验证模式，明天就能用在你的 agent 系统里。