Claude 没有证明黎曼假设。它得到的是一项重大但边界清楚的结果：Anthropic 一款尚未发布的研究模型给出无条件证明，至少三分之二的黎曼 ζ 函数非平凡零点位于临界线上；优化测试函数后，下界约为 67.25%。此前的无条件纪录略高于十二分之五，也就是约 41.67%。
比数字更值得研究的是验证架构。Anthropic 同时发布了完整论文、五页专家短注、Lean 4 形式化证明、审计记录和发现过程说明。这些工件组成一条分层证据链，每一层负责发现不同类型的错误。
形式化证明检查 Lean 中编码的命题能否从给定基础推出。专家审阅判断形式命题是否准确表达原数学问题，并核对它在已有研究中的位置。开放工件则让外部研究者重复这些检查。任何一层都无法独自替代其余层。
67.2% 究竟指什么
论文研究黎曼 ζ 函数的非平凡零点 (\rho = \beta + i\gamma)。黎曼假设要求所有这类零点的实部 (\beta) 都等于 (1/2)，也就是全部位于临界线上。
新结果给出的是 (T) 趋于无穷时的比例下界。核心结论包括：
- 至少三分之二的零点，按不同点计数，位于临界线上。
- 至少三分之二是临界线上的简单零点。
- 至少六分之五的零点互不相同。
- 使用优化后的 Montgomery-Taylor 测试函数，前两项提高到约 0.67250，不同零点的比例提高到约 0.83625。
这些结论是渐近、无条件的下界。方法没有把剩余约三分之一判定为临界线之外的零点，只是暂时无法为它们提供证书。论文也明确说明，这套方法无法判断完整黎曼假设的真伪。
因此，67.2% 既不是对前 67.2% 个零点的数值检查，也不是黎曼假设完成了 67.2%。它描述的是已经被证明的最低比例。
提升来自哪里
此前临界线零点比例的无条件纪录来自 Levinson 方法及其后续改进。论文引用的 2020 年结果超过 (5/12)，约为 41.66%。另一条研究路线来自 Montgomery 的零点对关联方法，它在假设黎曼假设成立时可以得到三分之二。
Baluyot、Goldston、Suriajaya 和 Turnage-Butterbaugh 近年的工作把对关联计算的素数侧变成了无条件结果。剩余困难位于零点侧：一旦允许零点偏离临界线，相关二次型就失去逐项正性。
Claude 的论文换了一种方式描述这个障碍。它把 Weil 的 Hermitian 形式限制在有限维函数空间中，再用线性代数读取其结构：
- 临界线上的零点贡献一个正的秩一形式。
- 一对对称的线外零点贡献一个签名为 ((1,1)) 的块。
- 素数侧提供一阶和二阶矩信息。
- Sylvester 惯性定律与 rank-trace 不等式把矩和签名转化为临界线零点数的下界。
创新点在于连接这两部分：用不定零点侧的线性代数结构，接上无条件的素数侧信息。组成材料大多已有研究基础，新的桥梁产生了新的下界。
四层验证栈
评估 AI 生成的数学结果，关键问题是每个工件具体验证什么。
| 层级 | 公开工件 | 能验证什么 | 仍需其他层处理什么 |
|---|---|---|---|
| 数学论证 | 完整论文 | 定义、引理、渐近推导、前人工作与方法边界 | 需要专家阅读和文献定位 |
| 专家压缩 | 五页技术短注 | 用较短路径呈现核心证明 | 省略了论文中的大量细节 |
| 形式命题与证明 | Lean 4 仓库 | 在固定 Mathlib 基础上，由内核检查 A 至 E 定理的推导 | 形式命题与原数学意图的一致性仍需语义审阅 |
| 复现与审计 | 仓库审计记录 | 工具链、依赖固定、sorry 与公理审计、comparator 流程 |
发布方审计仍值得外部团队独立复跑 |
仓库称，Zeta23/ 与 Solution 中的形式化没有 sorry，工具链固定为 Lean 4.33.0-rc2 和指定 Mathlib commit。公开审计记录显示，头部定理只依赖 Lean 的三项标准公理 propext、Classical.choice 和 Quot.sound。Comparator 另行在 Mathlib 上声明可信命题，核对命题等价，再用独立内核重放证明。
这些机制针对形式化证明常见的三类漏洞：关键定理被直接当作假设、证明中保留占位符、实现命题弱于对外宣称的命题。
独立复核者可以从冻结的 v1.0 release 开始，避免默认分支持续变化：
git clone --branch v1.0 https://github.com/anthropics/zeta-23-lean.git
cd zeta-23-lean
lake exe cache get
lake build
lake build Solution Solution.Multiplicity
lake env lean comparator/PrintAxioms.lean
lake env lean comparator/PrintAxioms/Multiplicity.lean
仓库记录显示，完整 Mathlib 依赖闭包包含数千个 build job，因此这是一项有实际资源成本的复现任务。它的关键价值在于输入、工具链、定理声明和预期审计输出都已显式化。
形式化的边界也需要同时写清。Lean 能高度精确地确认编码命题从编码基础中推出；数学家仍需确认定义、渐近口径和导入结果准确表达原问题。Anthropic 表示 Ralph Furman 与 Levent Alpöge 研究并验证了结果，Brian Conrey 与 Daniel Goldston 也审阅了论文。截至 2026 年 8 月 11 日，这项结果发布仅一天，外部学界的大范围独立审阅还处在早期阶段。
发现过程其实是一套搜索系统
Anthropic 披露，模型在两次 Claude Code session 中共产生 3100 万 output token。成功的一轮协调了约 60 个 subagent，执行约 2400 条 shell 命令，编写数百个 Python 脚本，用已知零点做数值检查，检索 54 篇 arXiv 论文，并让多个 Agent 互相审稿。
真正重要的是探索与验收被分开。
探索环允许高方差。数百个想法可以低成本失败；候选论证还要在黎曼假设类比为假的控制对象上接受测试；审查 Agent 被要求指出第一个无法成立的步骤。结果存活后进入更严格的验收链：独立重推、专家审阅、论文成稿、形式化、命题对照和公开工件。
这是一种数学 Agent 双循环协议。外循环追求搜索宽度，内循环严格限制哪些结果可以进入可信知识库。此前的数学 Agent 双循环验证协议讨论过同一结构。
它也解释了为什么仅看 AI transcript 无法验收数学发现。Transcript 记录行为；定理需要稳定命题、可复现推导，以及失败条件明确的验证接口。
AI 数学发现的最小验收协议
这次发布提供了一套可复用流程：
- 冻结命题：在宣称结果前固定量词、常数、渐近区间、计数口径和依赖。
- 分开探索证据与证明证据：数值实验和反例搜索用于筛选方向；只有被明确写入证明的内容才成为定理前提。
- 执行对抗审阅：让独立 Agent 和领域专家寻找第一个无效步骤，对照已知障碍，并测试相邻的反例系统。
- 形式化头部命题：固定证明助手与库版本，审计占位符、自定义公理、不安全声明和命题等价性。
- 公开失败面：说明方法无法证明什么、已经运行哪些检查、哪些环节仍依赖专家解释。
- 支持外部复跑：公开代码、原始文档、构建命令、版本哈希和必要过程信息。
这也是结果更广泛的意义。AI 可以生成大量候选数学，验证能力随之成为稀缺资源。有效的研究系统应优化错误的可检测性，而不是输出的说服力。
同一验证阶梯也适用于其他科学领域。在Claude 发现密码学弱点的案例中，可复现攻击与专家核验把合理猜测转化为安全结果。OpenAI 的单位距离问题研究面对的也是同一个核心问题：一项发现如何跨越为可信知识。
常见问题
Claude 证明了黎曼假设吗？
没有。完整假设要求全部非平凡零点位于临界线上。新定理证明的无条件下界约为 67.25%，剩余部分仍未获得证书。
从 41.6% 到 67.2% 改变了什么？
此前无条件纪录证明略多于十二分之五的零点位于临界线。新论证证明至少三分之二，优化测试函数后约为 67.25%。
有 Lean 证明以后还需要同行评审吗？
Lean 精确检查形式推导。专家评审检查形式命题是否对应原数学问题、定义与导入结果是否合适、创新性和文献定位是否准确。两者覆盖不同风险。
外部研究者能复现吗？
公开仓库固定了 Lean 与 Mathlib 版本，提供构建命令、公理审计和 comparator 配置。由于现有审计来自发布团队，独立复跑仍然有价值。
这对 AI 辅助科学意味着什么？
它展示了从大规模机器探索到窄化命题、专家审阅和机器可检验工件的完整链路。相比单一的 67.2% 数字，这条链路更容易迁移到其他研究问题。