Anthropic尚未发布的研究版Claude并没有解决黎曼猜想。它真正证明的是:在不依赖任何未经证明的假设的前提下,黎曼ζ函数三分之二以上的非平凡零点都是单零点,并且位于临界线上。31年来,这类结果的最佳纪录只从40%缓慢爬升到略低于42%。成果公布后短短几周内,人类数学家就已用更简洁的形式重写了这一证明,并把它推广到新的情形。这件事展示了AI能为研究型数学带来什么、它的能力边界在哪里,以及其背后的封闭模型为何招致批评。

零点为何重要

素数是不能拆分成两个更小整数相乘的整数。12可以拆成3乘以4,而7则完全无法拆分。素数是所有整数的基本构件,但它们在数轴上的分布并没有简单的规律。

1859年,伯恩哈德·黎曼证明,素数的位置由ζ函数的零点,也就是函数值为零的点所决定。人们常用管弦乐队来比喻这一点。平滑的估计值奏出基础旋律,每个零点则加入一道修正波。随着越来越多的零点加入,就像乐器一件件加入演奏,模糊的估计逐渐变得清晰,最终精确对应到每一个素数的位置。

另一个有用的比喻是调音台,每个零点对应一列控制单元。每一列都有一个旋钮,用来设定零点的高度,即虚部;还有一个推子,用来设定零点的实部。黎曼猜想断言,每个非平凡零点的推子都恰好停在二分之一的位置。这些推子排在一起,便构成一条直线,称为临界线。哪怕只有一个零点偏离这条线,和谐就会崩溃;克雷数学研究所的官方问题说明也警告,猜想一旦不成立,素数分布将陷入混乱。该研究所为证明或解决这一问题的人设立了$100万的千禧年大奖。

新结果还附加了一个条件:这些零点是单零点。单零点会独自穿过坐标轴,既不会与其他零点重叠,也不会只碰到坐标轴而不穿过。

验证12万亿个零点也不等于证明

计算机已检查了超过12万亿个零点,每一个都位于临界线上。但零点有无穷多个,这些工作只相当于一本无尽之书的第一页,算不上证明。因此,数学家转而寻求解析上的保证,即证明所有零点中必定位于临界线上的比例有一个下限。

年份 已证明位于临界线上的零点比例 证明者
1974年 超过三分之一(33.3%) 诺曼·莱文森
1989年 超过五分之二(40%) 布赖恩·康瑞
此后31年 略低于42%(十二分之五) 多篇论文
2026年 至少三分之二(66.7%),且为单零点 Claude

三十年的努力,平均每十年只让这一数字勉强提高一个百分点。Anthropic于8月10日公布了这一飞跃,并将其归功于数十年来人类数学家的前期研究。

成果是如何得出的

起因是Anthropic一名并非职业数学家的员工,让Claude认真尝试攻克黎曼猜想。Claude第一次独自尝试以失败告终。它提出了约650个不同的数学想法,没有一个奏效。

间隔约十天后,实验以另一种结构重新进行:一个自主运行的研究团队。一个Claude实例担任管理智能体,即负责规划和分派工作的AI进程,指挥约60个作为工作者的Claude副本。团队设置了多道防线来防止错误证明:

  • 仿冒函数测试。 每种技术还会被用于一些与ζ函数相似、但已知猜想在其上不成立的假函数。如果某种技术“证明”这类假函数的零点也全部位于临界线上,这种技术就会被判定为有缺陷。
  • 隔离式查错。 8月初,一个工作者报告称,至少50%的零点位于临界线上。管理智能体对此持怀疑态度,把论证拆成三部分,分别交给不同的智能体去找错。
  • 更进一步。 三部分都通过了这次相互隔离的审查后,那名员工要求系统以三分之二为目标。

接下来的进展并未按计划进行。管理智能体提出的方案行不通,而一个工作者另辟蹊径,写出了一个只有五行的新证明。这个工作者把证明保存到磁盘上,四分钟后因服务器API错误在一句话写到一半时崩溃。管理智能体随后从文件夹中找回了这个文件。那名员工还充当了啦啦队的角色,反复发送“继续”“相信自己”之类的消息,推动模型克服自我怀疑。

Anthropic公开了一份直接根据执行日志整理的详细记录,没有经过人工撰写或编辑。它也说明,这份记录中的中间计算没有经过外部核查。经过核查的是最终论文。

昏暗实验室中央的大发光球体向周围一圈约六十个小发光球体发出光束

▲ 指挥约60个工作者的管理智能体

两层检查

这一结果经过了两种验证。

  1. 人工审查。 Anthropic的两名数学家手工核对了论证。两人以自己的名义将论文提交到arXiv,把发现归功于Claude,并承担任何错误的责任。
  2. 机器检查。 Claude借助Lean的Mathlib库,把证明翻译成了Lean代码。Lean是一种证明助手,会依据严格的逻辑基础检查每一步推理。除Lean的三条标准公理外,Lean在没有任何未经证明的假设的情况下接受了这一定理。Anthropic的一名数学家确认,输入Lean的定义与论文中的表述一致。

外部数论学家布赖恩·康瑞和丹·戈德斯顿也在短时间内阅读了这篇论文。但这种阅读不等同于期刊接收。外部读者并没有正式认可这一证明,期刊同行评审仍在进行中。Lean检查也有局限:它能确认逻辑成立,却不能说明有人理解了这一结果为何成立。

去掉一个50年的星号

三分之二这个数字要追溯到1973年的休·蒙哥马利。蒙哥马利研究了零点的对关联,这是衡量零点聚集程度的指标。可以把它想象成打分:孤立的零点得1分,相互碰撞的零点得分更高。蒙哥马利证明,平均分至多为三分之四。平均分这么低,意味着每三个零点中至少有两个恰好得1分,也就是单零点。

但这里有个前提。蒙哥马利的论证假设黎曼猜想成立。大约50年来,这个星号一直没有去掉。

从2022年开始,丹·戈德斯顿和合作者改写了蒙哥马利的公式,使其不再依赖这一猜想。但要达到三分之二,仍需要另一个条件:所有零点都位于距临界线一根头发丝的范围内。偏离临界线的零点会以镜像对称的成对形式出现,因此在蒙哥马利的框架中,每一对这样的零点都会被计算两次。

Claude的论文回答了戈德斯顿团队提出的问题。它把这一框架与恩里科·邦别里2000年的一篇论文结合起来,去掉了接近程度的条件,从而得到一个完全不含未证明假设的三分之二定理。与其说AI独自超越了数学家,不如说它完成了人类多年来一直在推进的一条研究路线。

为什么这种方法无法证明整个猜想

Anthropic明确表示,它并不指望Claude的技术能证明黎曼猜想。原因在于方法本身。这种方法所依赖的性质,同样适用于那些零点确实偏离临界线的仿冒函数。因此,它无法把真正的ζ函数零点与零星散布在临界线之外的零点区分开来。对于这一整类被称为“带宽为一的证书”论证的方法,理论上限约为0.682,也就是大约68%。达到三分之二的新结果,似乎已经接近这一上限。

由人类让证明变得易懂

Claude的证明构造了一个与零点数量相匹配的巨大有限矩阵,并借助西尔维斯特惯性定律、联系矩阵秩与迹的不等式等工具推出估计。人类数学家认为它技术上错综复杂,缺乏直观性。后续研究很快出现:

  • arXiv发布四天后: 两名数学家把这套矩阵方法推广到本原狄利克雷L函数,这是与之相关的一类函数。
  • 9月2日: 洛林大学的一名数学家发表了另一个证明,用希尔伯特空间中的一个不等式取代了整个矩阵框架。这名数学家还证明,两个证明最终解决的是同一个极值问题。
  • 一周之内: 同一名数学家发布了修订版论文,补充了Claude的工作未涉及的关于相异零点的估计。
  • 随后不久: 另一名数学家用这一新方法,估计了临界线上短区间内零点的个数。

依赖庞大表格的机器证明可能掩盖其背后的结构,而把它们转化为更清晰的表述,似乎仍是人类数学家擅长的工作。

桌上一团纠缠的发光玻璃立方体格子逐渐散开,化为一条平滑的光带

▲ 从庞大矩阵到一个简洁不等式

封闭模型引发的开放性问题

这项研究使用的是未发布的Claude内部版本,因此Anthropic以外的任何人都无法测试或运行该模型。

2026年9月29日,高等研究院(IAS)的数学与人工智能咨询小组(AGMAI)发布了题为《负责任地发布AI生成的数学成果》的指南。这个由九名数学家组成、包括三名菲尔兹奖得主的小组,拒绝认可AI实验室用他人无法使用的专有模型检验重大猜想的做法。小组还拒绝了担任OpenAI顾问委员会的邀请,选择继续作为独立、无偿的监督机构。

指南要求,发布数学成果的实验室应在不受任何单一公司控制的中立存储库中公开以下内容:

  • 哪个模型完成了这项工作
  • 完整的提示词历史,即提供给模型的指令
  • 计算时间和资金成本
  • 经过验证的形式化证明

Anthropic公开了大量对话记录和Lean代码,但没有披露成本、确切的内部模型版本,也没有开放模型访问。咨询小组警告,封闭模型可能使数学界分裂为两个层级:企业实验室掌握突破性成果,而大学则被甩在后面。未来的数学工具是向所有人开放,还是留在企业的围墙之内,似乎取决于人类的选择,而非技术本身。

要点

Claude并没有证明黎曼猜想。但它把一个31年来停滞在42%以下的界限提升到了三分之二以上,而且证明通过了Lean检查。随后,人类数学家在几周内就简化并推广了这一结果。与其说这是AI单独取得的胜利,不如说是人类数论与机器形式化共同树立的里程碑。

下次再看到“AI解决了著名难题”的标题时,不妨检查以下四点:

  • 这项工作证明的是整个猜想,还是像界限这样的部分结果
  • 是否经过形式化验证,例如使用Lean,以及形式化定义是否与论文的主张一致
  • 期刊同行评审是否已经完成,还是只有非正式的阅读
  • 模型版本、提示词和计算成本是否已经公开

如果你自己也在用AI模型处理困难的技术问题,这项成果背后的工作方式提供了一些实用经验:

  • 把工作组织成由不同角色组成的智能体团队,而不是依赖一个冗长的提示词。
  • 用已知的反例或仿冒问题测试方法,尽早发现错误结果。
  • 让负责审查的智能体彼此隔离,以便它们独立判断各项主张。
  • 把中间发现保存到文件中,而不是只留在模型的上下文窗口里,以免崩溃时丢失。