Claude 没有证明黎曼假设：从 41.6% 到 67.2%，AI 科研闭环真正突破了什么？

摘要

Claude 没有证明黎曼假设，也没有把关键比例推进到 100%。Anthropic 披露的结果是：一个尚未发布的研究模型在既有数学工作的基础上，把“黎曼 ζ 函数非平凡零点位于临界线上的比例下界”从公开纪录 41.6% 推进到至少 67.2%。比数字本身更值得开发者关注的，是背后的研究型 Agent 闭环：长期任务、并行子 Agent、论文检索、代码实验、反例搜索、独立复核、Lean 形式化验证与人类专家审查共同工作。本文将从数字含义、系统架构、验证边界和工程实践四个层面拆解这次突破，并给出研究型 Agent 的落地检查清单。

1. 先纠正一个最容易出现的误读

如果只看社交媒体标题，这件事很容易被压缩成一句话：

Claude 攻克了黎曼假设。

这句话是错的。

黎曼假设讨论的是黎曼 ζ 函数所有非平凡零点的位置。假设成立，意味着这些零点全部落在实部为 1/2 的临界线上。换成这次报道采用的比例语言，真正解决黎曼假设对应的是 100%，而不是 67.2%。

三组数字必须放在一起看：

数字	准确含义	能否等同于证明黎曼假设
41.6%	此前公开结果给出的比例下界	不能
≥67.2%	Claude 研究过程得到的新下界	不能
100%	所有非平凡零点都位于临界线上	才对应黎曼假设成立

这里还有两个容易被标题抹平的限定词。

第一，67.2% 是至少 67.2%，它表达的是可证明的下界，不是在报告“已经检查完全部零点，其中 67.2% 合格”。

第二，Anthropic 对这项技术的定位也很克制：它并不被预期能够直接证明黎曼假设。也就是说，这是一项实质性的数学推进，但它与终极命题之间仍有明确边界。

对技术内容创作者和开发者来说，这个边界很重要。把“新的下界”写成“证明了黎曼假设”，不仅是标题夸张，还会掩盖真正值得研究的问题：一个 AI 系统究竟是怎样在开放、长周期、失败率极高的科研任务里产出可检查结果的？

2. 67.2% 是如何得到的

这项结果不是 Claude 从零开始发明了一套孤立理论。

公开材料显示，它建立在 Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh 等人的既有工作之上，同时使用了 Bombieri 在 2000 年提出的相关思路。Claude 所做的关键推进，是把这些此前分散的技术放进同一个函数空间和二次型框架中组合、优化，进而得到更强的比例下界。

这类工作更接近研究中的“重新表述与有效拼接”，而不是一句灵感突然解决百年难题。它至少包含三个层次：

1. 找到彼此可能兼容、但没有被直接组合过的已有结果；
2. 把它们翻译进统一的数学表示，使条件和目标能够共同计算；
3. 通过符号推导、数值实验和证明检查，判断组合后的改进是否真的成立。

这也解释了为什么“读过很多论文”不等于“会做研究”。检索只能提供候选材料，真正困难的是识别哪些结构可以兼容，哪些前提会冲突，以及组合后的对象能否经受反例和形式化检查。

因此，从开发者视角看，67.2% 不是一次更聪明的文本续写，而是一个复杂搜索过程最终留下的、经过多道筛选的候选结果。

3. 这不是一次聊天，而是一次长周期计算研究

把这次工作理解成“研究人员向 Claude 提了一个问题，模型回答了一篇证明”，会完全看错系统形态。

项目发起者 Jarred Sumner 本人并不是数学家。他给系统的是一个宽泛研究目标，而不是已经拆解好的证明路线。第一轮探索提出了大约 650 个想法，最后全部失败。失败并没有被从故事中删掉，因为它恰恰说明开放研究的常态：大多数路径不会通向结果。

随后，系统进入更长周期的计算研究阶段。公开材料披露的规模包括：

• 大约 60 个 Claude 子 Agent 协同；
• 约 2400 次 Shell 命令；
• 数百个 Python 脚本和大量数值检查；
• 两个 Claude Code 会话合计约 3100 万输出 token；
• 下载并检查 54 篇 arXiv 论文；
• 集中运行约一天半。

这些数字不是“越大越正确”的证明。它们说明的是另一件事：系统获得了远超单次对话的探索带宽。

一个候选方向可以被分派给不同子 Agent：有人尝试推导，有人搜索相关论文，有人写脚本做数值实验，有人专门寻找反例，还有人从头重建推理。失败路径、实验结果和中间结论被持续保存，后续 Agent 不必每次从零开始。

人类在主要运行阶段提供的输入很少，更多是鼓励系统继续推进。这意味着关键能力并不只是模型“知道多少数学”，还包括运行时能否让模型长时间保持任务状态、调用工具、拆解问题、吸收失败并组织复核。

但要再次强调：探索规模不等于可信度。60 个子 Agent 可以更快地产生候选思路，也可以更快地产生错误。真正决定研究结果能否被接受的，是后面那套验证链路。

4. 从 Base Model 到 Verifier：真正工作的系统是什么

如果要用工程语言概括这次系统，它至少包含四层，而不能只用“Claude 模型”一词带过。

层级	主要职责	在这次任务中的作用
Base Model	理解数学文本、提出推理和候选方向	生成证明思路、解释论文、修改推导
Agent Runtime	维持长周期状态，调度工具与子任务	管理会话、调用 Shell/Python、协调子 Agent
Harness	规定搜索、实验、记录和互审方式	保存失败、分配角色、组织反例搜索与独立复现
Verifier	对候选结果施加独立约束	数值检查、重建证明、Lean 检查、人类专家审阅

这四层的价值不同。

Base Model 决定系统能提出多高质量的局部推理；Agent Runtime 决定它能否跨越单次上下文窗口持续工作；Harness 决定搜索是否有秩序、失败是否能转化为信息；Verifier 则决定候选结果能否从“听起来合理”升级为“值得信任”。

这里最容易被误解的是 Lean。

Lean 可以检查：在给定定义、前提和形式化表达的情况下，每一步推理是否符合逻辑规则。它不能自动保证：

• 形式化时有没有遗漏原命题的重要条件；
• 输入 Lean 的前提是否真实、完整；
• 形式化对象与论文中的自然语言对象是否完全一致；
• 这个结果在数学史上是否真的新颖；
• 解释性文字有没有把一个局部结论夸大成更强命题。

所以，形式化验证很强，但它是验证链的一部分，不是一个覆盖所有科研风险的“绝对正确按钮”。

5. 为什么数学适合成为 AI 科研的第一站

AI 辅助科研可以进入很多领域，但数学具备几项特殊优势。

5.1 目标和失败条件相对清晰

很多数学问题有明确的命题、边界和反例结构。候选证明要么能连接关键步骤，要么会在某个条件上断裂。即使终极目标没有解决，中间结果也常能被精确描述，例如“把一个下界从 41.6% 提高到至少 67.2%”。

5.2 反馈成本相对低

数学探索可以大量借助符号推导、数值实验和小规模反例搜索。它不需要为每个候选想法都启动昂贵的湿实验，也不必等待数月才能观察结果。这让 Agent 可以快速经历“提出—检查—失败—修正”的循环。

5.3 知识已经高度数字化

论文、预印本、公式和证明文本大量存在于可检索语料中。系统能够读取前人工作，追踪引用，并对多个方法进行结构化比较。当然，能够访问文献不代表自动拥有正确理解，检索仍需配合推导和复核。

5.4 可以引入形式化证明系统

Lean 等工具提供了比自然语言自洽性更强的约束。模型不能只靠一段流畅解释蒙混过关，而要把推理落入机器可检查的逻辑对象。

这与编程有相似之处：代码可以运行，测试可以快速反馈，Agent 因而能持续迭代。但两者不能简单画等号。测试通过只说明覆盖到的案例符合预期，不等于程序在所有输入上正确；同样，数值实验支持一个数学猜想，也不等于已经得到证明。

6. 对 Agent 开发者意味着什么

这次案例对 Agent 工程最有价值的地方，不是告诉我们“模型参数再大一点就会成为数学家”，而是暴露出五个可以迁移的系统原则。

6.1 把开放目标拆成可验证的中间对象

“证明黎曼假设”几乎无法直接作为一个有效的执行单元。系统需要不断生成更小的对象：一个引理、一个函数空间、一组参数、一次数值检查、一条可能的反例。

中间对象越清晰，越容易并行，越容易失败，也越容易验证。研究型 Agent 的任务分解不应只回答“下一步做什么”，还应回答“下一步产物怎样被判定为无效”。

6.2 允许大量低成本失败

大约 650 个初始想法全部失败，并不意味着系统没有进展。只要失败原因被记录，后续搜索就能缩小空间。

真正危险的不是失败多，而是失败没有留下可复用信息：同一路径被重复尝试、错误前提被反复引入、负面结果无法传给其他 Agent。Harness 的核心职责之一，就是把失败变成结构化状态。

6.3 持久化过程状态，而不只保存最终答案

长周期研究需要保留论文线索、实验参数、脚本输出、已排除方向、未解决疑点和审查意见。只保存最后一段自然语言总结，会丢掉下一轮工作最需要的上下文。

因此，研究型 Agent 的记忆不应只是聊天记录，而应是可查询的研究账本。

6.4 用异构角色组织复核

让多个同构 Agent 同时生成答案，只能增加采样数量。更有效的做法是分配不同职责：提出者、反对者、复现者、文献审查者、数值实验者、形式化验证者。

角色之间的目标应当有意冲突。提出者希望推进候选方案，审查者则应以推翻它为目标。没有这种对抗性，所谓“多 Agent 互审”很容易退化成多次互相认同。

6.5 把 Verifier 当作一等公民

很多 Agent 产品先构建生成链，最后才补一个“请检查上述答案”的提示词。这远远不够。

Verifier 应该在任务设计之初就进入架构：哪些结论可由程序检查，哪些可以独立重算，哪些需要形式化工具，哪些必须由领域专家承担最终责任。验证预算也不应只是生成预算的尾数。

这个案例最值得复用的公式不是某条数学表达式，而是：

高探索带宽 + 可持久化的 Harness + 独立 Verifier + 人类责任边界

7. 构建研究型 Agent 时的检查清单

如果你正在设计一个用于科研、数据分析或高风险决策的 Agent，可以先用下面这份清单审视系统。

目标与停止条件

• 终极目标是否被拆成了可以单独检查的中间结论？
• 每条搜索路径在什么条件下停止，而不是无限消耗 token？
• 系统是否区分“没有找到反例”“数值上看起来成立”和“已经证明”？

独立复现与反例搜索

• 关键结果能否由另一个 Agent 或另一套脚本从原始输入重建？
• 是否有人专门寻找反例，而不是所有角色都在优化同一答案？
• 复现流程是否真正独立，还是继续读取了原推理中的隐含结论？

工具与过程可追踪性

• 论文来源、代码版本、参数、命令和输出是否可追踪？
• 失败路径是否结构化保存，避免后续重复踩坑？
• 每个重要结论能否追溯到证据、计算或明确的推理步骤？

新颖性检查

• 系统是否主动搜索已有论文、预印本和相邻表述？
• “没有检索到”是否被错误写成“此前从未有人提出”？
• 是否由领域专家判断结果的实际新颖性和价值？

形式化验证边界

• 形式化工具具体检查了哪些定义、引理和推理？
• 哪些前提来自外部，尚未被形式化系统验证？
• 自然语言结论与形式化命题是否逐项对齐？

最终责任

• 谁批准结果对外发布？
• 哪些结论仍需专家复核或公开同行评议？
• 出现错误时，是否能定位到责任环节并撤回结论？

这份清单并不意味着任何团队都能低成本复刻 Anthropic 的运行规模。它的价值在于帮助你判断：当前系统是在扩大候选答案的数量，还是已经建立了与探索规模匹配的可信机制。

8. 现在仍不能宣布“AI 数学家”诞生

这项工作很重要，但现在就宣布“AI 数学家已经诞生”，证据仍然不够。

首先，完成任务的研究模型尚未公开。外界无法在相同条件下复现整套过程，也无法判断哪些能力来自模型本身，哪些来自特定 Harness、算力投入和人工准备。

其次，探索成本很高。约 60 个子 Agent、3100 万输出 token 和大量工具调用，展示的是一种高预算研究形态，而不是普通开发者今天就能复制的工作流。它证明了能力上限的可能方向，并没有证明单位结果成本已经可接受。

再次，目前主要验证仍来自 Anthropic 内部。Brian Conrey 和 Dan Goldston 做过简短审阅，但这不同于长期、公开、多人参与的同行评议。数学共同体还需要时间检查证明、边界与新颖性。

最后，Lean 的加入提高了可信度，却没有消除所有人工判断。形式化定义是否准确、前提是否充分、自然语言主张是否越界，仍然需要数学家负责。

因此，更稳妥的判断是：我们看到了一个 AI 系统在高水平数学研究中产生非平凡候选结果，并建立了比普通聊天机器人更完整的验证链。它离“自主、稳定、低成本、可公开复现的 AI 数学家”还有距离。

9. 结论：失败的终极任务，也可能产出真实的新结果

Claude 没有解决黎曼假设。它面对终极目标时失败了，而且第一轮大约 650 个方向也全部失败。

但科研并不只有“解决终极问题”与“毫无价值”两个状态。在既有工作的基础上，把一个关键比例下界从 41.6% 推进到至少 67.2%，如果经过后续公开审查仍然成立，就是一项真实的中间成果。

对 AI 行业而言，更重要的变化也许是科研工作流本身：Base Model 提供推理能力，Agent Runtime 提供持续执行能力，Harness 把失败和协作组织起来，Verifier 与人类专家守住可信边界。

AI 正在显著扩大可探索的假设数量，但信任并不会因为搜索变快而自动变便宜。越能生成，越需要独立复现、反例搜索、形式化工具和专业审查。

这才是这次突破最值得开发者记住的部分：不是“Claude 已经证明了黎曼假设”，而是我们第一次更清楚地看到，一个研究型 Agent 如何在没有完成终极任务的情况下，仍然沿着可验证的路径产出有价值的新结果。

参考资料

1. Anthropic：Claude and the Riemann hypothesis
2. Anthropic 公开技术材料（一）
3. Anthropic 公开技术材料（二）
4. Anthropic 公开技术材料（三）
5. Anthropic：zeta-23-lean
6. Anthropic 官方发布信息