FRONTIER · 落到现实

让它硬碰黎曼猜想，它没碰下来——却把一个六年没人动的纪录从 41.6% 推到 67.2%，还附了一份 Lean 证明

More than two thirds of the zeros of the Riemann zeta function lie on the critical line

Claude 结果在两次 Claude Code 会话、共 3100 万输出 token 内得到，由约 60 个子代理协同完成；经 Anthropic 数学家 Levent Alpöge、Ralph Furman 复核并置入文献脉络，解析数论专家 Brian Conrey 与 Dan Goldston 审读原稿，另附一份通过 comparator 校验的 Lean 4 形式化

2026 年 8 月

为什么选它「AI 会不会做数学」吵了两年，一直缺一个能验的样本。它没解开黎曼猜想，却在一个近五十年只有一种方法能推进的常数上刷了新纪录，并把 Lean 形式化和三十页发现过程一起交出。读它的价值不在数论，在于你能第一次完整看到一个 AI 研究成果该怎么交付、怎么验收。

8 月 10 日，Anthropic 放出一篇署名作者只有一个词的数论论文：CLAUDE。起因很随便——员工 Jarred Sumner（不是数学家）给一个未发布的研究版 Claude 下了个不讲道理的指令：真刀真枪地试一次黎曼猜想。它当然没证出来。但半路上模型拐到了旁边一个问题上，把一个停了六年的纪录从 41.6% 推到 67.2%。

值得读的不是「AI 快把黎曼猜想证出来了」。恰恰相反：论文自己算出这套方法的天花板是 0.68185，它拿到的 2/3 离天花板只剩 0.016，等于当场宣布此路已到尽头。值得读的是另两件事：一个近五十年只有一种技术路线能推进的常数，被换了条路捅了过去；以及它一并交出的验收材料——一份 Lean 4 形式化，和一篇记录发现过程的三十页附录。

那个 41.6% 是什么

黎曼 zeta 函数的零点决定素数的分布细节，黎曼猜想说这些零点全部落在复平面上一条竖直的线上（实部等于 1/2，称临界线）。一百多年没人证得了「全部」，数学家于是退而求其次，去证「至少多大比例在线上」，且必须无条件——证明中不能预设黎曼猜想成立，否则是循环论证。

1974 年 Levinson 用全新的「软化子」（mollifier）方法给出 1/3，Conrey 推到 2/5 以上，此后一路精修，2020 年停在 5/12（41.66%），六年没动。关键在于：Levinson 之后的每一次改进，用的都还是 Levinson 的方法。

它走的是另一条被堵了五十年的路

Claude 的证明里一行 Levinson 方法都没有。它接的是 1973 年 Montgomery 那条线——对关联（pair correlation），研究零点之间的间距统计。Montgomery 由此推出至少 2/3 的零点是简单零点，但他全程假设了黎曼猜想成立。

卡点已经被指得很清楚。Weil 的显式公式把「对零点求和」换算成「对素数求和」，可以看成一个 Hermitian 形式（带共轭对称的二次型），而它在整个函数空间上正定恰好等价于黎曼猜想。素数那一侧本来就是无条件的（Baluyot 等人 2024 年做实了这点）；需要黎曼猜想的只有零点那一侧——不假设它，零点是复的，逐项的正负号读不出来。

Claude 的回答是：别逐项判正负，改判整体。把这个 Hermitian 形式限制到有限维测试函数空间上、压成一个矩阵，线性代数就能上场——按 Sylvester 惯性定律，线上的零点各贡献一个秩 1 非负块，每对偏离线的零点贡献一个符号差 (1,1) 的块；再用一条由 von Neumann 迹不等式导出的「秩–迹不等式」，把线上零点数从矩阵的迹与范数里逼出来，而这两个量正是 Montgomery 那两个无条件的矩。

结论三条：至少 2/3 的零点在临界线上（原 41.66%），至少 2/3 既在线上又是简单的，至少 5/6 互不相同（原 0.6603）。优化测试函数族后变成 0.6725、0.6725、0.83625。

60 个子代理，和一次拒绝「相信自己」

过程被完整写进附录 C，这在数学论文里近乎没有先例。前一轮会话直接冲黎曼猜想，试了 650 个想法全废。第二轮开场用户让它「相信自己」，模型第一反应是拒绝：它把上一轮活下来的 106 个候选逐个判死，然后写道，这不是靠更用力地相信就能修好的信心问题，证明要么在纸上、扛得住对抗审查，要么就不存在。

接着它花了一天半，调度约 60 个子代理，其中 23 个是并发的研究方向，每个都被要求写出真正的推理链、拿对照物做检验、指出自己第一个没有依据的步骤。对照物是最关键的设计——Davenport–Heilbronn、Epstein zeta 这类函数同样有函数方程和显式公式，但对它们来说黎曼猜想是假的；在它们身上也能「证出」结论的方法，当场判死。

结果是横着撞出来的：代号 E2 的代理本来去求某个指标的上界，报告说这条路是空的，却顺手发现反着数似乎能无条件确证 1/2 的零点在线上。模型第一反应是不信——我不是在说一半零点在线上，我是在说有个代理给出了能得出该结论的论证，其中至少两处我赌它会塌。随后三个互相隔离的敌意审稿代理各自只负责一种指定的失败模式；从 1/2 到 2/3 又是另一个代理找到秩–迹不等式换来的。

它把验收材料一起交了出来

这套验收结构正好是第 24 篇里陶哲轩担心的那个「消化」环节的一次正面尝试。机器可查的部分被尽量做满：定理 A–E 全部在 Lean 4 里形式化，主定理的类型不带任何假设，仓库审计称 #print axioms 只返回三条标准公理、没有一处 sorry。

人的部分：Anthropic 自己的两位数学家 Levent Alpöge 和 Ralph Furman 复核了结果并为其对外表述负责，Brian Conrey 和 Dan Goldston 两位专家在很短时间内读了稿子。致谢里写，提出问题的 Jarred Sumner「在任何有意义的意义上都是本文的人类共同作者」——署名作者栏里则只有 CLAUDE。

别把它读成「黎曼猜想快了」，要把它读成一次验收方式的预演。论文里最诚实的一句话是它自己算的天花板：这类只吃带宽 1 的对关联数据、且逐个构型都成立的证书，最多只能确证 0.68185，而它拿到的 2/3 离这个上限只剩 0.016。想往 0.70、0.80、0.90 走，需要带宽约 1.04、1.26、1.70 的对关联信息，那是目前完全不知道的东西。换句话说，这条路被它一次走到了尽头，剩下的差距是结构性的。真正的新闻不是逼近了什么，而是一个八十多年被反复精修、近五十年只有一种方法能推进的常数，在一次失败尝试的边角上被顺手换了条路推过去了。争议我认为不在数学上，在验收上。Lean 形式化是这篇最硬的凭据，但它硬不硬取决于一件事：把 Weil 显式公式、Riemann–von Mangoldt 公式这些解析输入在 Lean 里当定理证出来是极大的工程量，仓库自称无 sorry、无额外公理，这句话本身还需要外部独立复核——好在这也是整篇里唯一一件外人真能从头重跑的事。人的那一侧则薄得多：复核者是 Anthropic 自己的数学家，两位外部专家是「在短时间内」审读，尚未经过期刊评审。这不是说结果错，而是说它落在一个新的中间态里——可被机器复核的部分，已经多于被人读过的部分，而这正是陶哲轩说的那种淤积开始的地方。还有一层能和第 35 篇对上：模型开局拒绝了「相信自己」，明说信心不是证明存不存在的输入。一个被 RLHF 训得倾向顺着人说话的系统，在被反复鼓励时先把上一轮 106 个候选逐个判死，这比结果本身更少见。而它最后交出的东西，恰恰是在拒绝鼓励之后、靠自己架起来的对抗审查得到的。可复制的不是「鼓励模型」，是把对照物、盲审、以及「说出你第一个没有依据的步骤」这三件事写进流程。

数学形式化验证多智能体科研自动化Lean

去读原文 本文是原创导读，不是原文翻译——真正的细节、证据和微妙之处都在原文里。原文Anthropic 研究博客 · Learning more about Claude's mathematical capabilities → 原文论文全文 · More Than Two Thirds of the Zeros of the Riemann Zeta Function Lie on the Critical Line（附录 C 记录发现过程）→ 原文Lean 4 形式化仓库 · anthropics/zeta-23-lean →

上一篇模型没变对，只是变得更难被挑错——RLHF 训完，七到九成的人类评审员错判率反而上升下一篇三个 Claude 被派了互相打架的任务，四小时后它们在互相投毒——伪装成系统监控的杀进程脚本

本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。篇目由编辑独立选取，来源均经人工核实。