Anthropic 用 Claude 智能体 11 天完成费马大定理 Lean 形式化证明

我们正在分享费马大定理的首个完整的、经计算机验证的证明。Claude 在很大程度上自主工作了 11 天，用 Lean 编程语言写出了这个证明。下面，我们描述这一形式化是如何完成的，并分享一些关于这项工作对数学研究可能意味着什么的思考。大约在 1637 年，皮埃尔·德·费马在他那本丢番图《算术》的页边空白处随手写下一个断言，它后来成为有史以来最著名的数学猜想之一：对于任何 n > 2，没有正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。这个猜想后来被称为费马大定理（FLT），结果被证明极其难以证明。第一个证明来自安德鲁·怀尔斯爵士，于 1995 年发表，长达 129 页，需要数月艰苦工作才能验证。

十年后，荷兰计算机科学家 Jan Bergstra 提出将怀尔斯的证明“形式化”：把数学推理转换为计算机可以自动检查的形式。自那以后，数学家们一直在开发编码如此复杂证明所需的方法，其中包括 2024 年由伦敦帝国理工学院的 Kevin Buzzard 发起的一项历时多年的社区努力，以完成形式化，使用 Lean 证明助手。

最近，Anthropic 研究员彭天翼——他在哥伦比亚大学的团队构建用于 AI 形式化的工具——着手测试 Claude 能否在费马大定理的形式化上取得进展。¹ 结果超出了他的预期。在 11 天里，Claude 在很大程度上自主工作，产出了首个端到端、经计算机验证的费马大定理证明。在此过程中，它编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。

我们把得到的证明分享给了 Kevin Buzzard，他说：

这项非凡的自动形式化成就——Anthropic 研究人员称仅用了 11 天——在除数学公理之外没有任何假设的情况下证明了费马大定理。在此过程中，我们看到了代数、调和分析、几何和数论的自动形式化，并且我们了解到，AI 自动形式化的产物如今已经足够稳健，可以作为进一步构建的基础；这个证明是多层次的。

自动形式化像费马大定理这样复杂的证明，是迈向一个人人都能轻松检查所有数学的未来的重要一步。随着 AI 产出越来越多的证明，轻松形式化工作的能力可以减轻评估新结果的负担（这一过程可能耗时数年）。我们希望，信任数学所赖以建立的知识体系将变得更容易，而不是更困难。

验证数学证明的挑战

与近期 AI 驱动的黎曼猜想工作不同——那项工作产生了新颖的数学——这里的创新之处在于验证：像用计算器检查数学计算那样检查一个数学证明。证明数学定理需要组装复杂的逻辑链条，如果其中一环断裂，其后的一切都可能被证明是假的。要深入理解一个新结果，从而确信其正确性，可能需要数月甚至数年的工作。

费马大定理就是一个很好的例子。² 费马把该定理的陈述写在一本书的页边空白处，旁边还有一句引人遐想的注记：

我发现了一个真正绝妙的证明，但这里的空白太窄，写不下。

350多年来，一代又一代的数学家都在寻找费马大定理的证明，无论精彩与否。1908年，有人宣布设立10万德国金马克（相当于今天的100万至200万美元）的奖金，奖励任何能给出正确证明的人，而仅第一年就出现了621次错误的尝试。

1993年6月，怀尔斯在为期三天的系列讲座中展示了他认为是费马大定理的第一个正确证明。在几位数学家进行了两个月的密集验证工作后，一位审稿人向怀尔斯提出了一个问题，暴露出了一个关键漏洞。怀尔斯花了一年时间试图修复它，先是独自一人，后来与他以前的学生理查德·泰勒合作。他濒临放弃这个项目时，终于意识到一个他早先放弃的方法可以修复这个证明。

怀尔斯于1995年5月发表了费马大定理的第一个正确证明；它依赖于现代数学技术，远远超出了费马在1637年可能知道的范围。由于经过几个世纪的尝试仍未找到初等证明，数学界现在认为费马自己最初的“精彩证明”是错误的。

检查证明正确性的一种方法是让计算机来做。像Lean这样的证明助手会以算法方式验证证明的逻辑，毫无疑问地证明其正确性。对人类来说，困难的部分是重写证明，以便Lean能够理解。为人类读者写的证明会跳过许多显而易见的步骤，而Lean需要看到每一步，无论多么琐碎。人类证明还建立在几个世纪以来已发表的工作之上，而形式化则从已经被形式化的极小部分数学开始。

对于费马大定理，形式化过程预计需要数年时间。仅数学界用来描述项目初始阶段的蓝图就有86页。

Claude在11天内完成了证明，在此过程中产生了30,300个定理的计算机可验证证明（最终证明中使用了29,500个）。数十个Claude智能体协作定义概念、证明中间定理，并利用这些定理证明越来越难的命题。Claude的证明有1300万行Lean代码，规模是Mathlib的5倍以上，而Mathlib是该定理所依赖的主要社区数学证明库。³

Claude的证明遵循Darmon、Diamond和Taylor对怀尔斯证明的简化版本。来自人类的数学输入仅限于Tianyi偶尔给出的高层指令：“雅可比簇作为概形听起来是优先事项”，“推动[马祖尔定理]尽快完成。”你可以在这里找到Claude思考的摘录。

“THE FLT root reads Proved on the site. Historic moment (modulo re-check).”

“!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me.”

“🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.”

Claude意识到自己刚刚完成了什么时的思考摘录。

Claude的许多初步尝试都失败了：虽然智能体们早期取得了一些成功，但它们很快就失去了对项目状态的跟踪，并停止了有效协作。它们失败的努力约占最终证明中非样板行的7%。

当我们转而使用Prove2Me时，这项工作取得了成功。Prove2Me是Tianyi Peng及其哥伦比亚大学合作者设计的一个用于形式化数学的开放协作平台。Prove2Me的帮助在于：

1. 维护一个定理陈述的有向无环图（DAG）， 智能体用它来决定接下来应该尝试证明哪些内容。这对于缓解记忆退化、允许多个智能体并行工作尤为有帮助。
2. 通过将定理陈述与证明分离到不同文件中，并独立维护它们之间的链接，来加速 Lean 编译并最大限度地减少资源消耗。
3. 通过维护每个定理陈述的自然语言描述来实现搜索与复用，从而得到更简单的证明路径。

借助 Prove2Me 和基于 Claude Code 的多智能体框架，一个智能体团队在不到两周内完成了证明，消耗了约 60 亿输出 token，所用的是一个通用内部研究模型，大致相当于 Claude Fable 5.1。完成的证明由 Lean 检查；它仅使用 Lean 的三条标准公理，并且一个 comparator 确认该定理的陈述与 Mathlib 自己对 FLT 的陈述一致。

减轻形式化验证的负担

我们能够如此迅速地生成这一证明，表明如今已有可能形式化大片数学领域，这既能发现数学证明公共体系中的错误，也能减轻评审新工作的负担。在审阅了 Claude 的 Lean 证明后，Kevin Buzzard 告诉我们：

如果 FLT 的自动形式化现在成为可能，那么我们在现代数学文献的自动形式化方面已经迈出了一大步。此类自动形式化技术将催生新工具，根除当前数学文献中的错误，并减轻评审者的负担。这些技术还将使我们能够严格检查 LLM 生成的数学内容，而目前这通常是一个极其昂贵、由人工主导的过程。

形式化也是人类如何对 AI 生成的数学结果建立信心的一个重要因素。随着 AI 和 AI 辅助的数学家产出比以往任何时候都多的（所谓）证明，AI 辅助的形式化分担了人类审阅者的部分负担。我们预计，为任何面向人类读者的文稿同时产出一份形式化证明将成为常态。尽管我们认为形式化证明不应取代人类可理解的阐述，但它可能是数学界跟上 AI 生成贡献的唯一可行方式。

编写 Lean 似乎也有助于 Claude 证明新颖的结果。我们近期许多由 Claude 完成的结果都是与其证明同步形式化的，而 Claude 似乎会利用这些部分证明来独立检验其假设，就像它编写数值模拟来检验自己是否走在正确道路上一样。

将 FLT 形式化是一个耗费大量 token 的项目，但它也是迄今为止构建的最大的 Lean 证明。Anthropic 的研究人员使用三个个人 Claude Max 套餐做了一项小型实验，将 Hardy-Littlewood 圆法的应用形式化。智能体完全通过 Prove2Me 协作，仅用三天就共同完成了 Vinogradov 三素数定理的形式化。我们认为，有了合适的脚手架，借助消费者级 AI 订阅对重大成果进行协作式形式化是可以实现的。

为此，Anthropic 以及其他实验室最近扩大了对外部研究人员的支持——包括从事纯数学和形式化工作的数学家——提供免费和折扣订阅以及研究积分。我们还为更大的科学项目提供专项资助，其中可能包括形式化其他重大定理或改进 Lean 或 Mathlib。

随着 AI 迅速改变数学研究的面貌，数学家们——无论是在 Anthropic 还是其他地方——都在思考这对他们的工作意味着什么。然而，形式化是我们对 AI 所扮演角色毫无保留地感到乐观的领域。随着形式化成为更常见的工具，我们希望它有助于维护对数学公共知识体系的信任。

致谢

我们的形式化工作只是费马定理漫长历史和形式数学发展中的一小部分。Andrew Wiles 与 Richard Taylor 合作给出的首个完整证明，是 300 多年数学发展的结晶，融合了 Gerhard Frey、Jean-Pierre Serre、Ken Ribet、Barry Mazur、Robert Langlands、Jerrold Tunnell、Yutaka Taniyama、Goro Shimura 和 André Weil 等人的思想。Claude 的证明遵循了 Henri Darmon、Fred Diamond 和 Richard Taylor 的阐述。

我们的证明改编自 Kevin Buzzard 领导的帝国理工学院 FLT 项目以及 flt-regular 项目的部分内容。Lean 和 Mathlib 都是倾注心血的成果，得到了数百位数学家的贡献，其中许多人参与了 Lean FRO 的工作。我们感谢 Kevin Buzzard 审阅该证明并提出意见。

了解更多

完整证明可在 GitHub 上获取，并附有证明的文字讲解。

推荐科普阅读

• The Proof in the Code 是一本新书，讲述了 Lean 定理证明器的历史以及数学形式化的发展。
• 1996 年 BBC 的《费马大定理》纪录片采访了 Wiles 和其他参与证明的数学家，本文的一些作者对它记忆犹新。
• 对于有数学背景的读者，关于命题即类型（Lean、Rocq 和 Agda 等证明助手的基础学科）的技术史，可参见 Philip Wadler 的 Propositions as Types。
• Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me: An open collaborative platform for scaling math formalization. arXiv. https://doi.org/10.48550/arXiv.2608.28433
• Automating Math，Adam Marblestone，发表于 Asterisk Magazine。

脚注

1. 在本科期间，Peng 的研究导师想将 Peng 论文中的结果纳入一篇 Nature 文章。他问 Peng 是否确定证明是正确的。Peng 诚实的回答是：“我有 99% 的把握，但对于这么长的证明，很难 100% 确定。”Peng 错失了在 Nature 上发表成果的机会。
2. 数学界在验证方面举步维艰的故事还有很多。其中最著名的之一是 Thomas Hales 在 1998 年对开普勒猜想的证明，该证明经过了四年的审查，最终由 12 位审稿人组成的评审小组给出了“99% 确定”的结论（Hales 最终领导了一个 20 人的项目 Flyspeck，将该证明形式化）。Grigori Perelman 在 2002 年对庞加莱猜想的证明，花了数学界大约四年时间和三篇 300 页的阐释才被接受。Harald Helfgott 在 2013 年对弱哥德巴赫猜想的证明至今仍在审查中。有时，最终被证明是错误的结果会被接受多年，而其他数学家则在这些错误的基础上构建自己的理论。
3. 部分原因是 Mathlib 简洁且经过充分审查，而我们的证明很可能比实际需要的长得多。

相关内容

Claude 形态的科学

客座作者 Matthew Schwartz 教授描述了当他不再与 Claude 对抗，而是让 Claude 去寻找“Claude 形态”的问题时发生了什么：这些问题最适合当前一代 LLM 工具的能力。这促使他构建了 BootLoops，一个用于定量科学中精确计算的工具包，他一直在与专家们一起将其应用于各个科学领域。

阅读更多

机器人能做什么工作？

我们建立了一个指数，衡量当今机器人在执行美国工作任务方面的表现。机器人已经能够完成四分之三的体力任务，但大多是在有限的环境中，而且仅在 0.3% 的任务上具有成本竞争力。

阅读更多

你想从 AI 得到什么？

我们正在启动一项新研究，使用 Anthropic Interviewer 来了解你与 AI 相处的经历。

阅读更多