Anthropic 自己不期望 Claude 使用的技术证明黎曼猜想。黎曼猜想认为,黎曼 zeta 函数的每个非平凡零点都位于实部为二分之一的临界线上,这个猜想仍未得到证明。Anthropic 更窄的主张依然重大。Claude 的一个未发布研究版本给出了无条件证明,把位于该线上的零点占比已知下界从 41.6% 提高到 67.2%。这是对渐近占比的下界,不是所有零点都在该线上的证明,也没有说明其余零点在哪里。
新闻价值在于跃升幅度。Anthropic 的论文称,41.6% 的纪录自 2020 年保持至今。按照公告中的四舍五入数字,Claude 在一项结果中把纪录提高了 25.6 个百分点。论文列出的历史进展中,没有任何一次改进接近这个幅度。证明大量借鉴了 Baluyot、Goldston、Suriajaya 和 Turnage-Butterbaugh 的成对关联研究,也使用了 Bombieri 的早期工作。新步骤是用线性代数重新解读这套方法,通过一个二次型同时处理临界线上和线外的零点。结果延伸了人类数学,而不是脱离人类数学凭空出现。
这套验证比听起来可信的模型记录更强。Anthropic 发布了基于 Mathlib zeta 函数定义的 Lean 4 形式化证明,并称它通过标准 comparator,没有未完成证明占位符。Anthropic 数学家 Levent Alpöge 和 Ralph Furman 研究并验证了结果。Brian Conrey 和 Dan Goldston 在很短时间内从外部审阅了论文。Conrey 自己的工作就在临界线下界的经典历史中,因此他的审阅具有分量。但界限仍需说明:发布模型、论文和验证说明的都是 Anthropic。外部审阅不等于独立的同行评审出版。
人类提供的火花异常小而具体。Bun 的创建者、非数学家 Jarred Sumner 要求 Claude 认真尝试黎曼猜想。Anthropic 称,模型最初尝试了 650 个想法但都失败,随后用一天半协调大约 60 个子代理。在 31 million 个输出 token 中,它们执行了 2,400 条 shell 命令,检查候选论证并互相审阅工作。Sumner 的输入主要是鼓励信息。随后 Claude 搜索反例,下载 54 篇论文检查新颖性,并独立重新证明该结果。这些数字描述的是一次昂贵的研究运行,不是可重复的 benchmark。
真正有后果的部分不是励志轶事,也不是模型品牌,而是一个推动百年下界的具体定理。它带有机器可检查的工件,也附有制造者明确写出的限制。研究模型尚未发布,因此外部研究者还不能测试这种能力能否泛化。披露材料只有 Anthropic 这一个来源,因此更广泛的数学界仍需仔细检查证明及其新颖性。如果结果经受住这一过程,它就应进入数论记录。这不会让黎曼猜想减少半分未解状态。
