Claude 将黎曼ζ函数临界线上零点比例下界从 41.6% 推进至 67.2%
Anthropic 发布消息称，研究版 Claude 参与的未公开研究将黎曼ζ函数临界线上零点的无条件比例下界从约41.6%提升到约67.2%，并配套论文与 Lean 形式化代码。该结果并非黎曼猜想的证明，仍需数学界同行评审与验证。
Anthropic 发布消息称，研究版 Claude 参与的未公开研究将黎曼ζ函数临界线上零点的无条件比例下界从约41.6%提升到约67.2%，并配套论文与 Lean 形式化代码。该结果并非黎曼猜想的证明，仍需数学界同行评审与验证。
Anthropic 8月10日公布，一项由尚未公开发布的研究版 Claude 参与完成的数学研究，将“黎曼ζ函数有多少零点位于临界线”这一相关问题的已知无条件下界，从约 41.6% 提高到约 67.2%。
这并不是对黎曼猜想的证明。黎曼猜想要求证明所有非平凡零点都位于实部为 1/2 的临界线上，而 Anthropic 明确表示，这项工作只证明了至少约三分之二的零点位于该直线上，距离 100% 仍有本质差距。
Anthropic 在官方说明中称，研究版 Claude 在 Claude Code 的两次工作过程中发现了这一结果。相关论文、面向专家的简要说明，以及 Lean 形式化证明也已公开。
从黎曼猜想到“至少有多少零点在临界线上”
黎曼猜想由德国数学家波恩哈德·黎曼在1859年提出。它关注黎曼ζ函数的非平凡零点，而这些零点与素数分布之间存在深刻联系。猜想认为，所有非平凡零点的实部都等于 1/2。
尽管这一猜想至今没有被证明或推翻，数学家已经证明了越来越高比例的零点位于这条临界线上。此前的纪录是由长期的解析数论研究逐步推进至 5/12，也就是约 41.67%。Anthropic 的论文将新的结果表述为：在适当的极限意义下，至少约 0.6725 的零点位于临界线；官方说明将其四舍五入为 67.2%。
这类“比例下界”与“猜想被证明”是两件不同的事。下界只能说明已经确认的部分至少达到某个比例，不能说明剩余零点也一定在临界线上。因此，67.2% 并不是黎曼猜想的概率，也不是对所有零点位置的最终判断。
Claude 的新结果建立在既有数学研究上
论文标题为《More than two thirds of the zeros of the Riemann zeta function lie on the critical line》。论文摘要称，研究在不假设黎曼猜想成立的情况下，证明了至少三分之二的零点位于临界线，并在优化测试函数后得到约 0.6725 的常数；论文还给出了关于简单零点和互异零点的相关结论。
从数学方法看，这不是 Claude 凭空创造出一套全新的黎曼猜想理论。Anthropic 表示，结果结合了 Baluyot、Goldston、Suriajaya 和 Turnage-Butterbaugh 等人的近期工作，以及 Bombieri 在2000年的研究。核心变化，是把此前依赖于临界线正定性的分析，转化为对 Weil 二次型有限维压缩的线性代数分析。
通俗地说，位于临界线上的零点可以贡献正定部分，而成对出现在临界线外的零点会形成具有相反符号的结构。研究者随后利用矩阵的秩、迹和惯性等信息，估计临界线部分的规模。论文称，正是这种不把整个函数空间简单对角化、而是同时处理正负定子空间的做法，使新的下界成为可能。
完整技术内容见 Anthropic 发布的结果论文。论文仍需更广泛的数学界同行审阅，才能判断其技术论证是否会被学界接受为正式的纪录推进。
约60个子代理参与了探索过程
Anthropic 说，Claude 最初提出并尝试了650个思路，但都没有成功。随后，研究版 Claude 在约一天半的时间里协调了大约60个子代理，执行了约2400条 Shell 命令，并编写数百个 Python 脚本。
这些子代理进行了数千次数值检查，检验已知的ζ函数零点，互相审查证明，寻找反例，并下载54篇 arXiv 论文，以确认结果此前没有被发表。Claude 还从头独立重做了证明，并建议由人类数论专家审查其发现。
整个过程累计产生约3100万输出 token。Anthropic 的官方说明指出，任务发起者 Jarred Sumner 是公司员工，但不是数学家；他的主要作用是不断要求 Claude 继续尝试，而不是为模型提供具体的数学路线。
这一过程呈现出一种与传统“模型给出答案”不同的研究工作流：模型负责提出假设、搜索文献、运行实验、分派子任务和反复质疑自己的论证，人类专家则需要判断这些步骤是否构成可靠且有意义的数学证明。AIFlux 此前对科学计算进入 agentic AI 时代、但验证成为新瓶颈的报道，也涉及类似变化：当生成和执行变得更便宜，验证、责任归属和长期维护会成为更难的部分。
Lean 形式化证明提供了另一层检查
Anthropic 数学家 Levent Alpöge 和 Ralph Furman 研究了 Claude 的工作，以理解新结果与既有研究之间的关系。Anthropic 还表示，Claude 与员工 Eric Easley 合作，把结果转化为 Lean 形式化证明，并通过标准验证工具 comparator 检查。
相关代码已发布在 anthropics/zeta-23-lean 仓库。仓库 README 称，项目包含论文主要定理的 Lean 4 / Mathlib 形式化版本，顶层定理没有额外假设，仓库本身也没有声明项目专属公理。仓库的审计记录称，形式化代码在固定版本的 Lean 和 Mathlib 上完成构建，核心定理的 #print axioms 结果只显示 Lean 的三个标准逻辑公理。
但形式化通过并不自动等于整篇论文已经获得同行评审。Lean 可以检查被编码进系统的命题和证明步骤是否符合形式逻辑，却不能替代学界对研究问题、定理表述、先前成果引用和论证意义的全面审查。形式化代码覆盖的范围、依赖的数学库以及是否准确对应论文中的每个关键步骤，同样需要专家进一步检查。
这类“AI生成、机器验证、人类解释”的分工，也与 Anthropic 近期让 Claude 参与密码学研究的尝试形成呼应。此前，Claude 曾被用于寻找 HAWK 和减轮 AES 的新攻击路径，但相关结果同样需要专家审查，并不能简单等同于现实系统已经被攻破。对于数学研究而言，问题则变成：模型能否提出真正的新想法，以及人类能否及时理解、验证并将这些想法纳入可复用的知识体系。
黎曼猜想仍然没有被解决
Anthropic 在官方说明中写道，公司并不认为 Claude 使用的技术会导向黎曼猜想本身的证明。此次结果的重要性，首先在于它显著提高了一个长期存在的无条件下界；其次在于它展示了一种由大模型协调文献检索、数值实验、反例搜索、证明写作和形式化验证的研究流程。
但目前能确认的结论仍应保持在有限范围内：一项由 Anthropic 发布、并已配套论文和 Lean 代码的研究，声称将临界线零点比例的已知下界提高到约 67.2%至67.25%；黎曼猜想没有被证明；独立的数学同行评议仍然是判断最终学术影响的下一步。
在更广泛的 AI 科学研究竞赛中，这或许比“模型是否解决了一个世纪难题”更能说明问题。Claude 没有跨过黎曼猜想的最后一道门槛，但它在一条由人类数学家铺设的路径上推进了一个重要的中间结果。接下来，真正的检验将不只是数字能否从 41.6% 上升到 67.2%，而是数学界能否独立复核这项证明，并判断它能否被其他研究者继续使用。
来源：
不错过任何一条 AI 大事
订阅 AIFlux 早报，每天 3 分钟看懂产业动态。
