一款尚未发布的 Anthropic 模型在数学最大未解难题之一上取得进展

150 多年来，黎曼猜想一直是数学领域最重要的未解问题之一。它是一个关于素数分布的长期谜题。目前，能够给出该猜想有效一般性证明的人可获得100 万美元奖金，但这笔奖金至今仍无人领取。

当代 AI 模型同样尚无法解决这一问题——但它们能够取得的进展远超人们的预期。这一发现很可能重新引发一个长期存在的问题：当代 AI 是否具备发现新的科学和数学思想的能力。

周一，Anthropic 宣布，一款尚未发布的模型在黎曼猜想上取得了显著进展，大幅提高了已知满足该猜想的解的下界。

更令人印象深刻的是这一进展的实现方式：一名没有深厚数学训练背景的 Anthropic 员工要求该模型“认真尝试”证明这一猜想，随后让模型在接下来约一天半的时间里自行协调这项任务。

总体而言，该模型测试了 650 种不同的解题思路，协调了 60 个子 Agent，并累计消耗了 3100 万个输出 token。

论文的一则脚注解释道：“在 60 个子 Agent 中，有两名负责发展关键数学思想；13 名向这两名 Agent 提供思路；30 名尝试（但未能）发展新的思路；13 名担任验证者，检查论证的正确性；最后两名则帮助撰写初始论文。”

这一发现得到了 Anthropic 两名内部数学家的确认，并利用开源证明助手 Lean 完成了形式化。

这是由大语言模型（LLM）推动的一系列数学突破中的最新一项。今年以来，AI 模型已经解决了一批 Erdős 问题，而更强大模型的发布也带来了更令人瞩目的成果。OpenAI 最近发布了由其内部“Astra”模型证明的 10 项重大结果；与此同时，Anthropic 的另一项研究工作推翻了长期存在的 Jacobian 猜想。

不断积累的研究成果同时在数学界引发了兴奋与担忧。在一份于 6 月签署的公开声明中，一批知名数学家担心，AI 可能会削弱这一领域的重要价值观——尤其是数学证明应当“可归属于具体作者，这些作者为其发现获得认可，并为其正确性承担责任”的标准。

但对于数学家应如何运用这些新研究技术，该领域仍存在分歧。在一篇回应该声明的博客文章中，菲尔兹奖得主 Timothy Gowers 质疑，AI 的影响是否可能以更复杂且积极的方式改变数学。

Gowers 写道：“如果我们进入一个数学定理不再与数学家关联的世界，那么这或许并不比恒星不以天文学家命名——而且大多数恒星根本没有名字——更加成问题。”

For more than 150 years, the Riemann hypothesis has stood as one of the major unsolved problems in mathematics, a long-running mystery about the distribution of prime numbers. There is currently a $1 million bounty for a working general proof of the hypothesis, which remains unclaimed.

Contemporary AI models still can’t solve it either — but they can make a lot more progress than you might expect, a finding that’s likely to reopen longstanding questions about contemporary AI’s ability to discover new scientific and mathematical ideas.

On Monday, Anthropic announced that an as-yet-unreleased model had made significant progress on the Riemann hypothesis, significantly increasing the lower bound of solutions for which the hypothesis holds true.

Even more impressive is how the progress was made: An Anthropic staff member without significant mathematical training prompted the model to “take a real stab” at proving the hypothesis, then left the model to coordinate the task across the following day and a half.

All told, the model tested 650 different ideas for solving the problem, coordinating across 60 subagents and spending 31 million output tokens in total.

“Out of the 60 subagents, two were responsible for developing the key mathematical ideas,” a footnote to the paper explains, “13 contributed ideas to these agents, 30 attempted (but were unable) to develop new ideas, 13 served as validators to check the correctness of the arguments, and the final two helped to write the initial paper.”

The finding was confirmed by two of Anthropic’s in-house mathematicians, and formalized using the open source proof assistant Lean.

This is the latest in a string of mathematical breakthroughs led by large language models, or LLMs. A number of Erdos problems have been solved by AI models over the course of this year, and the release of more powerful models has led to more impressive results. OpenAI recently released a set of 10 major results proved by its internal “Astra” model, while a separate effort from Anthropic disproved the longstanding Jacobian conjecture.

The growing body of results has caused both excitement and concern in the mathematical field. In a public declaration signed in June, a group of prominent mathematicians raised concerns that AI could undermine critical values of the field — particularly the standard that true mathematical proofs should be “attributable to specific authors who take credit for their discovery and assume responsibility for their correctness.”

But the field is still split on how mathematicians should approach the new research techniques. In a blog post responding to the declaration, Fields Medal winner Timothy Gowers questioned whether the influence of AI might change mathematics in a more complex and positive way.

“If we arrive at a world where mathematical theorems are no longer associated with mathematicians, maybe that won’t be any more problematic than the fact that stars aren’t named after astronomers and most aren’t named at all,” Gowers wrote.