费马大定理的形式化证明

科学

费马大定理的形式化证明

2026年9月4日

我们在此分享首个经计算机完整验证的费马大定理证明。Claude 在 11 天里基本自主完成了这份用 Lean 编程语言撰写的证明。下文将介绍这次形式化的具体过程，并谈谈这项工作对数学研究可能意味着什么。

大约在 1637 年，皮埃尔·德·费马在自己那本丢番图《算术》的页边写下了一个论断，后来成为数学史上最著名的猜想之一：对任意 n > 2，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。这个后来被称为费马大定理（FLT）的猜想极难证明。Andrew Wiles 爵士于 1995 年给出了第一个证明，长达 129 页， Verification 花费了数月的艰苦核对工作。

十年后，荷兰计算机科学家 Jan Bergstra 提出对 Wiles 的证明进行“形式化”：把数学推理转换成计算机可以自动验证的形式。此后，数学家们一直在发展编码如此复杂证明所需的方法，其中包括 2024 年由伦敦帝国理工学院的 Kevin Buzzard 发起的多年社区协作，目标是用 Lean 证明助手完成这一形式化。

最近，Anthropic 研究员 Tianyi Peng（他在哥伦比亚大学的团队致力于构建 AI 形式化工具）想测试 Claude 能否在 FLT 形式化上取得进展。¹结果超出了他的预期：Claude 在 11 天内基本自主工作，产出了首个端到端、经计算机验证的 FLT 证明，过程中编写了 1300 万行 Lean 代码，证明了 29500 个中间定理。

我们把最终证明分享给了 Kevin Buzzard，他说：

Anthropic 研究人员表示，这项非凡的自动形式化成就仅耗时 11 天，它在不加任何假设（仅依赖数学公理）的情况下证明了费马大定理。在此过程中，我们见证了代数、调和分析、几何与数论的自动形式化，并了解到 AI 自动形式化产物已足够稳健，足以作为进一步构建的基础；该证明具有多层结构。

自动形式化像费马大定理这样复杂的证明，是迈向未来数学可轻松验证的重要一步。随着 AI 不断产出更多证明，轻松形式化研究成果的能力可以减轻评估新结果的压力（这一过程往往耗时数年）。我们期待，建立在其上的数学知识体系将变得更容易而非更难获得信任。

数学证明验证的挑战

与近期的 AI 驱动黎曼猜想工作不同——后者产生了新的数学内容，这里的创新点在于验证——就像用计算器复核数学运算一样去核查数学证明。证明数学定理需要组装复杂的逻辑链条，一旦其中一环断裂，后续所有推论都可能是错误的。深入理解一个新结果并确信其正确性，往往需要数月甚至数年的工作。

费马大定理就是一个典型的例子。²费马在书页边距中写下了该定理的陈述，并附有一句诱人的注脚：

我已发现一个真正美妙的证明，但这个页边太窄，写不下。

在长达 350 多年的时间里，几代数学家一直在寻找费马大定理的证明，无论是否如费马所言那般美妙。1908 年，有人宣布为任何能给出正确证明的人设立 10 万德国金马克奖金（相当于今天的 100–200 万美元），而在第一年就有 621 个错误尝试被提交。

1993年6月，怀尔斯在为期三天的系列讲座中呈现了他认为首个正确的费马大定理（FLT）证明。几个月来多位数学家正进行密集的验证工作，此时一位审稿人向怀尔斯提了一个问题，暴露出证明中存在一个关键漏洞。怀尔斯花了整整一年试图修补，起初独自攻关，随后与前学生理查德·泰勒合作。就在他即将放弃该项目时，终于意识到自己早些时候曾摒弃的一种方法能够修复证明。

怀尔斯于1995年5月发表了FLT的第一个正确证明，它依赖于远超1637年费马所能知晓的现代数学技术。由于历经数世纪 Attempts 仍未找到初等证明，数学界如今认为费马本人所谓的“奇妙的证明”是不成立的。

费马大定理的形式化

检验证明正确性的一种方式，是让计算机来执行。Lean 等证明辅助工具能够通过算法验证证明逻辑，从而无可辩驳地展现其正确性。对人类而言，困难的部分在于将证明重写为 Lean 可以理解的形式。面向人类读者的证明会跳过许多显然的步骤，但 Lean 需要看到每一步，无论多么平凡。此外，人类证明建立在几个世纪发表的研究成果之上，而形式化却只能从零起步，基于已被形式化的数学中那极小一部分。

对于 FLT，形式化过程预计需要数年。仅数学界用于描述项目初始阶段的蓝图就有 86 页。

Claude 在 11 天内完成了证明，期间生成了 30,300 个定理的可机检证明（最终证明使用了其中的 29,500 个）。数十个 Claude 代理协同工作，定义概念、证明中间定理，并利用这些定理去证明越来越难的命题。Claude 的证明长达 1300 万行 Lean 代码，超过其赖以构建的核心社区数学证明库 Mathlib 规模的 5 倍有余。³

Claude 的证明遵循 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化版本。人类的数学输入仅限于 Tianyi 偶尔给出的高层指令，比如“Jacobian 作为 scheme 听起来优先级很高”“尽快把 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 之后，这项工作才得以成功。这是由 Tianyi Peng 及其在哥伦比亚大学的合作者设计的一个开放协作的数学形式化平台。Prove2Me 的帮助主要体现在：

1. 维护定理陈述的有向无环图（DAG），智能体据此决定下一步尝试证明什么。这对缓解记忆退化、支持多个智能体并行工作尤为关键。
2. 加速 Lean 编译并降低资源消耗，方法是把定理陈述和证明分拆到不同文件中，二者之间的关联独立维护。
3. 支持搜索与复用，为每个定理陈述维护一份自然语言描述，从而得到更简洁的证明路径。

借助 Prove2Me 以及基于 Claude Code 的多智能体框架，一组智能体在不到两周的时间内完成了证明，消耗了约六百亿个输出 token，使用的是与 Claude Fable 5.1 大致相当的内部通用研究模型。最终证明经 Lean 校验通过；仅使用了 Lean 的三个标准公理，且一个 比较器 确认定理陈述与 Mathlib 中 FLT 的陈述一致。

减轻形式化验证的负担

我们能以如此速度完成这份证明，表明如今形式化大段数学内容已成为可能，这既能发现现有数学证明体系中的错误，也能减轻对新工作的审稿负担。审阅了 Claude 的 Lean 证明后，Kevin Buzzard 向我们表示：

如果现在能够实现 FLT 的自动形式化，那么我们就在实现现代数学文献自动形式化的道路上迈出了重要一步。此类自动形式化技术将催生新工具，清除当前数学文献中的错误，并减轻审稿人的负担。这些技术还将使我们能够严格检查由大型语言模型生成的数学内容，而目前这通常是一个极其昂贵的、由人工主导的过程。

形式化也是人类对 AI 生成的数学结果建立信心的重要因素。随着 AI 和 AI 辅助数学家生成的（所谓）证明前所未有地增多，AI 辅助形式化承担了部分人工审查的工作。我们预计，任何面向人类读者的说明性文章都将伴随一份形式化证明。虽然我们认为形式化证明不应取代人类可理解的阐释，但它可能是数学界跟上 AI 生成贡献的唯一可行途径。

编写 Lean 代码似乎也帮助 Claude 证明了新的结果。我们近期由 Claude 撰写的许多成果都在证明过程中同步完成了形式化，Claude 似乎会利用这些部分证明独立检查其假设，正如它编写数值模拟以验证方向是否正确一样。

形式化费马大定理是一项耗时巨大的项目，但它也是迄今为止规模最大的 Lean 证明。Anthropic 的研究人员进行了一项小规模实验，使用三个个人版 Claude Max 订阅来形式化 Hardy-Littlewood 圆法的应用。通过 Prove2Me 平台完全协作，这些代理仅用三天就共同完成了文戈拉多夫三素数定理的形式化。我们认为，借助合适的框架，使用消费者级 AI 订阅协作形式化重大成果是可行的。

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

随着 AI 快速改变数学研究的面貌，数学家们——包括 Anthropic 内外的许多人——正在思考这对他们的工作意味着什么。但要说 AI 的角色，形式化是我们唯一感到毫无疑虑、由衷认可的领域。随着形式化逐渐成为常用工具，我们希望它能帮助维护数学公共知识体系的可信度。

致谢

我们的形式化工作只是费马定理漫长历史和形式化数学发展中的一小步。Andrew Wiles 与 Richard Taylor 的首个完整证明，是三百多年数学积累的集大成之作，融合了 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 纪录片《Fermat's Last Theorem》收录了对 Wiles 及其他参与证明的数学家的采访，本文部分作者对它有着美好的回忆。
• 对于有数学背景的人，Philip Wadler 的 Propositions as Types 一文提供了命题即类型（命题助手如 Lean、Rocq 和 Agda 的底层学科）的技术历史。
• 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 后来领导了一个由二十人组成的小组，即 Flyspeck，对该证明进行了形式化）。Grigori Perelman 在 2002 年对 庞加莱猜想 的证明，则花费了社区大约四年时间以及三篇 300 页左右的阐释文章才被接受。Harald Helfgott 在 2013 年对 弱哥德巴赫猜想 的证明目前仍在审稿中。有时一些后来被证明是错误的结果会被 接受多年，而其他数学家则在此基础上构建自己的理论。
3. 这部分是因为 Mathlib 简洁且经过充分审查，而我们的证明很可能比实际需要冗长得多。