Claude 用 11 天完成费马大定理的首个完整机器验证证明

我们正在分享费马大定理的首个完整计算机验证证明。Claude 在 11 天内基本自主完成了这项工作，用 Lean 编程语言写出了证明。下面，我们将介绍这一形式化工作的完成过程，并分享这项工作对数学研究可能意味着的一些思考。

大约在 1637 年，皮埃尔·德·费马在他那本丢番图《算术》的页边空白处写下了一个论断，这个论断后来成为有史以来最著名的数学猜想之一：对于任何 n > 2，不存在正整数 a、b、c 使得 aⁿ + bⁿ = cⁿ。费马大定理（FLT），即这个猜想后来为人所知的名字，被证明是极其难以证明的。第一个证明由安德鲁·怀尔斯爵士于 1995 年给出，长达 129 页，并且花费了数月艰苦细致的工作才得以验证。

十年后，荷兰计算机科学家扬·贝格斯特拉提出“形式化”怀尔斯的证明：即将数学推理转化为计算机可以自动验证的形式。自那时起，数学家们一直在开发对这种复杂证明进行编码所需的方法，其中包括一项由伦敦帝国理工学院的凯文·巴扎德于 2024 年发起的多年社区合作项目，旨在使用 Lean 证明助手 完成该证明的形式化。

最近，Anthropic 研究员、同时在哥伦比亚大学领导一个构建 AI 形式化工具小组的彭天翼，着手测试 Claude 是否能在形式化 FLT 方面取得进展。¹结果超出了他的预期。在 11 天内，Claude 基本自主地完成了工作，产出了 FLT 的首个端到端、计算机验证的证明。在此过程中，它编写了 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 需要看到每一步，无论这一步多么琐碎。人类的证明还建立在数百年来已发表成果的基础之上，而形式化工作则只能从已被形式化的那一小部分数学出发。

就费马大定理而言，形式化过程原本预计需要数年时间。仅数学界用来描述该项目初始阶段的 blueprint 就长达 86 页。

Claude 在 11 天内完成了这一证明，期间产出了 30,300 条定理的计算机可验证证明（最终证明中使用了其中 29,500 条）。数十个 Claude 智能体协同工作，共同定义概念、证明中间定理，并利用这些定理去证明难度越来越高的命题。Claude 的证明包含 1300 万行 Lean 代码，规模是 Mathlib（该定理所依托的主要社区数学证明库）的 5 倍以上。³

Claude 的证明遵循了 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化版本。来自人类的数学输入仅限于 Tianyi 偶尔给出的高层指令，例如：“将 Jacobian 作为概型处理似乎是高优先级事项”，“推动 Mazur 定理尽快完成”。你可以在此处查看 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，这些 token 来自一个与 Claude Fable 5.1 大致相当的通用的内部研究模型。完成的证明已通过 Lean 校验；它仅使用了 Lean 的三个标准公理，并且一个 比较器 确认该定理的陈述与 Mathlib 中 FLT 的陈述一致。

减轻形式化验证的负担

我们能够如此迅速地完成这一证明，表明现在形式化大量数学内容已成为可能，这既可能发现常见数学证明体系中的错误，也可能减轻审阅新研究成果的负担。在审阅了 Claude 的 Lean 证明后，Kevin Buzzard 告诉我们：

如果费马大定理（FLT）的自动形式化如今已成为可能，那么我们就向现代数学文献的自动形式化迈出了一大步。这类自动形式化技术将催生新工具，帮助剔除当前数学语料中的错误，并减轻审稿人的负担。这些技术还将使我们能够严格检验大语言模型生成的数学内容，而目前这一过程通常需要耗费极高的人力成本。

形式化也是人类对 AI 生成的数学结果建立信心的一个关键因素。随着 AI 及 AI 辅助的数学家产出的（声称的）证明比以往任何时候都多，AI 辅助的形式化工作分担了人类审稿人的部分负担。我们预计，未来在面向人类读者的任何文稿旁边同时附上一份形式化证明将成为常态。尽管我们认为形式化证明不应取代人类可理解的阐述，但它可能是数学界跟上 AI 生成成果步伐的唯一可行途径。

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

将费马大定理形式化是一个消耗大量模型 token 的项目，但它也是有史以来规模最大的 Lean 证明。Anthropic 的研究人员做了一项小实验，使用三个个人版 Claude Max 套餐来形式化哈代-李特尔伍德圆法的应用。这些智能体完全通过 Prove2Me 协作，在短短三天内共同完成了 维诺格拉多夫三素数定理 的形式化。我们认为，只要有合适的脚手架，利用消费级 AI 订阅来协作形式化重大成果是可以实现的。

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

随着 AI 迅速改变数学研究的面貌，数学家们——无论是在 Anthropic 还是在其他地方——都在思考这对他们的工作意味着什么。然而，在形式化方面，我们觉得 AI 的作用是毋庸置疑地积极的。随着形式化成为一种更常见的工具，我们希望它将有助于维护对数学知识共同体的信任。

致谢

我们的形式化工作是费马定理漫长历史与形式数学发展中的一小部分。安德鲁·怀尔斯与理查德·泰勒共同完成的首个完整证明，是三百多年数学发展的集大成之作，融合了格哈德·弗雷、让-皮埃尔·塞尔、肯·里贝特、巴里·马祖尔、罗伯特·朗兰兹、杰罗尔德·特内尔、谷山丰、志村五郎以及安德烈·韦伊等人的思想。Claude 的证明遵循了亨利·达蒙、弗雷德·戴蒙德和理查德·泰勒的论述路径。

我们的证明借鉴了伦敦帝国理工学院 FLT 项目（由凯文·巴扎德领导）以及flt-regular 项目的成果。Lean 和 Mathlib 本身就是两项倾注心血的事业，数百位数学家为其做出了贡献，其中许多人还与Lean FRO合作。我们感谢凯文·巴扎德审阅该证明并提出意见。

了解更多

完整证明已在GitHub上公开，并附有一份书面的证明讲解文档。

推荐阅读材料

• 《代码中的证明》是一本近期出版的著作，讲述了 Lean 定理证明器的历史以及数学形式化的发展。
• 1996 年的 BBC 纪录片《费马大定理》采访了怀尔斯及其他参与证明的数学家，本文的几位作者对它记忆犹新。
• 对于有数学背景的读者，可以在 Philip Wadler 所著的 《命题即类型》中找到命题即类型（Lean、Rocq 和 Agda 等证明助手背后的基础学科）的技术发展史。
• Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me：一个用于规模化数学形式化的开放协作平台. arXiv. https://doi.org/10.48550/arXiv.2608.28433
• 《数学自动化》，Adam Marblestone 著，发表于《Asterisk》杂志。

脚注

1. 在本科期间，Peng 的导师想把 Peng 论文中的成果收录进一篇 《自然》文章。导师问 Peng 是否确定证明是正确的。Peng 诚实的回答是：“我有 99% 的把握，但这么长的证明很难做到 100% 确定。”Peng 因此错过了让自己的成果发表在 《自然》上的机会。
2. 数学界在验证方面挣扎的故事还有很多。其中最著名的当属托马斯·黑尔斯（Thomas Hales）1998 年对开普勒猜想的证明，该证明经过四年审查，最终由 12 位审稿人组成的评审组以“99% 确信”收场（黑尔斯最终领导了一个 20 人项目 Flyspeck 将该证明形式化）。格里戈里·佩雷尔曼（Grigori Perelman）2002 年对庞加莱猜想的证明，学界大约花了四年时间、三篇各 300 页的阐述才予以接受。哈拉尔德·赫尔夫戈特（Harald Helfgott）2013 年对弱哥德巴赫猜想的证明至今仍在审查中。有时，最终被证明是错误的结论竟会被接受多年，其他数学家便在这些错误的基础上构建自己的理论。
3. 这在一定程度上是因为 Mathlib 简洁且经过充分评审，而我们的证明很可能比实际需要的要冗长得多。