Claude 把黎曼 zeta 下界从 41.6% 推到 67.2%:60 个 subagent、31M tokens、Lean 形式化的一次"数学工地"预演

黎曼猜想本身没破,但围绕它的"数学工地"刷新了工作方式。Anthropic 8 月 10 日发了一篇博客,披露一支未公开研究版的 Claude 在挑战黎曼猜想的过程中,意外把一个相关长期未动的下界记录从 41.6% 推到了 67.2%(anthropic.com/research/riemann-zeta)。这条结果有意思的不是数字本身,而是数字是怎么算出来的——一个非数学背景的 Anthropic 员工 Jarred Sumner 写下"take a real stab"一句提示词,Claude 用了 31M output tokens、协调约 60 个 subagent、跑了 2,400 条 shell 命令,反复交叉检验数千个零点,最后还写出 Lean 形式化证明通过验证。

这不是"AI 直接做科研",而是"AI 工地"的协同编排

第一次会话里 Claude 试了 650 个想法全部失败,第二次会话重组为多智能体集群:2 个负责核心数学想法,13 个贡献想法,30 个尝试后没能产出新想法,13 个做校验,最后 2 个负责写初稿,合计 60 个 subagent。每个 subagent 之间会相互审稿对方的论证、搜索反例、独立从零重新推导(anthropic.com/research/riemann-zeta)。整个流程里 Jarred 的输入被官方报告调侃为"主要发一些鼓励——'keep going' 和 'believe in yourself' 的各种变体"。

这意味着这次结果真正展示的不是一个模型的智力上限,而是多智能体编排+工具调用+长上下文一致性+形式化证明落地这套组合,在一个具体的数学子问题里第一次跑出了可见产出。

67.2% 这个数字意味着什么

这里补充一点数学背景。黎曼 ζ 函数零点中,被认为落在临界线上的最小比例,几十年里数学家从零开始把它推到了 41.6%。这次的 67.2% 不是证明黎曼猜想本身,而是把"已知的、至少在临界线上的零点占比下界"刷新了一大截。结合 Aryan(2019)、Baluyot-Goldston-Suriajaya-Turnage-Butterbaugh(2023、2025)、Bombieri(2000)等几篇前置工作的成果,Claude 的关键动作是"把整个二次型空间、正定与负定子空间放在一起处理,并允许非对角二次型"——这一"敢把整体空间一把梭"的勇气,直接带来了下界突破(anthropic.com/research/riemann-zeta)。

更重要的一条工程事实是,Anthropic 自己的两位数学家 Levent Alpöge 和 Ralph Furman 复查并产出了一份给同行的非形式化说明,同时 Claude 与工程师 Eric Easley 一起产出了 Lean 4 形式化证明,通过标准 comparator 工具校验(github.com/anthropics/zeta-23-lean)。Lean 这一步的作用是把"听起来对"的论证锁死成可机器检查的证明——一旦 comparator 通过,任何人随便重跑都能复现。

为什么这次更像"工作流 demo",而不是"模型突破"

把这件事放在 LLM 能力曲线里看,有两点值得拎出来说。第一,Anthropic 在文末明确说"我们不指望 Claude 用到的技巧能证明黎曼猜想本身"。这家公司没有把这个结果包装成 AGI 跃迁,而是诚实地把它定位成"AI 数学能力最新进展的一个例子"(anthropic.com/research/riemann-zeta)。第二,Anthropic 自己也承认,Claude 一开始对能不能做出有意义进展是怀疑的——它从训练里学到了"开放数学难题很难、AI 模型也有局限"。换句话说,Claude 是被一段鼓励性的提示词(anthropic 在脚注中提到同样的 prompt 套路之前用于证明 Jacobian conjecture)推着走出了自我怀疑,才最终拿到结果。

这给我们一个比"AI 做数学"更值得讨论的视角:当前阶段的 LLM,在开放式数学研究里,真正稀缺的不是推理深度,而是一套能支撑它持续推进、交叉验证、形成可发表产出的工作流——Subagent 编排、长程记忆、工具调用、Lean 这种形式化校验,缺哪一环,650 个想法死在第一个会话的结局就会重演。

给行业的启发

从写 LLM 工作流的工程师视角看,这次最值得抄的不是 31M tokens 或者 60 个 subagent 这些数字本身,而是三层闭环:第一层,subagent 之间互相 referee,而不是单 agent 内部 self-check;第二层,下载 54 篇 arXiv 论文做查新——对外对比"这个结果是不是已经有人做过";第三层,Lean 形式化作为最后一道闸门,即便专家已经审过,仍用机器校验固化结论(github.com/anthropics/zeta-23-lean)。这三层组合,大概就是接下来一段时间 AI 辅助科研要拼的标准动作。

至于黎曼猜想本身,这次显然没解出来。但一份配 Lean 形式化、两位数学家复核、查过 arXiv 没撞车的 67.2% 下界证明,本身就是 AI 在严肃数学里能留下的少数可被同行评议的产出物之一。下一步,真正的看点是:哪家公司能把这一套多智能体数学工地的工作流产品化,让非数学背景的工程师也能用上。

参考链接:Anthropic 官方博客、Lean 形式化代码库。