Anthropic 未发布模型在黎曼猜想上取得进展
Anthropic 未发布模型仅凭员工一句提示，自主协调数十个 AI 子代理在黎曼猜想上取得实质进展，引发学界对 AI 科研能力的重新审视。
黎曼猜想是数学界最重要的未解难题之一，关乎素数分布规律，至今无人证明。Anthropic 一个未发布模型在提示下，自主协调 60 个子代理、测试 650 种思路，显著提升了该猜想成立解的下界，并用 Lean 证明助手完成形式化验证。这再次引发 AI 能否发现新数学思想的讨论。
正文摘录
150 多年来，黎曼猜想 (Riemann hypothesis) 一直是数学界未解的重大问题之一，这是一个关于素数分布的长久谜团。目前，该猜想有一个 [100 万美元的悬赏](https://www.claymath.org/millennium/riemann-hypothesis/)，奖励能给出完整通用证明的人，但至今无人认领。 当代 AI 模型同样无法解决它——但它们取得的进展远超你的预期。这一发现很可能将重新引发关于当代 AI 发现新科学和数学思想能力的长期争论。 [本周一](https://www.anthropic.com/research/riemann-zeta)，Anthropic 宣布，一个尚未发布的模型在黎曼猜想上取得了重大进展，显著提高了该猜想成立解的下界。 更令人印象深刻的是取得进展的方式：Anthropic 一位没有深厚数学背景的员工，提示模型"认真尝试"证明该猜想，然后让模型在接下来的一天半时间里自主协调这项任务。 总共，该模型测试了 650 种不同的解题思路，协调了 60 个子代理 (subagent)，共消耗了 3100 万个输出 token (output token)。 论文脚注解释称："在 60 个子代理中，有 2 个负责提出了关键的数学思想，13 个为这些代理贡献了想法，30 个尝试（但未能）提出新思路，13 个作为验证者检查论证的正确性，最后 2 个帮助撰写了初稿论文。" 这一发现得到了 Anthropic 内部两位数学家的确认，并使用开源证明助手 [Lean](https://lean-lang.org/) 进行了形式化验证。 这是大语言模型 (LLM) 主导的一系列数学突破中的最新成果。