Anthropic 用 Claude 在 11 天内完成费马大定理首个机器验证的 Lean 形式化证明

我们公布了费马大定理的首个完整计算机验证证明。Claude 在 11 天内基本自主地完成了这项工作，用 Lean 编程语言写出了证明。下面，我们介绍这一形式化工作的具体做法，并分享一些关于这项工作对数学研究可能意味着什么的思考。大约在 1637 年，皮埃尔·德·费马在他那本丢番图《算术》的页边空白处写下了一个论断，这个论断后来成为有史以来最著名的数学猜想之一：对于任何 n > 2，不存在正整数 a、b、c 使得 aⁿ + bⁿ = cⁿ。费马大定理（FLT），即这个猜想后来为人所知的名字，被证明是极其难以证明的。第一个证明由安德鲁·怀尔斯爵士于 1995 年给出，长达 129 页，并且耗费了数月艰苦的验证工作。

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

近日，Anthropic 研究员田一鹏（Tianyi Peng）——他在哥伦比亚大学的团队致力于构建 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 需要看到每一步，无论多么琐碎。人类的证明还建立在数百年已发表成果的基础之上，而形式化工作则只能从已被形式化的那一小部分数学知识开始。

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

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

视频 · 前往原文观看

FLT 形式化的时间推进

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 后，这项工作取得了成功。Prove2Me 是一个由哥伦比亚大学的 Tianyi Peng 及其合作者设计的开放协作式数学形式化平台。Prove2Me 的助力体现在：

维护一个定理声明的有向无环图（DAG），智能体据此决定下一步应尝试证明哪些定理。这对于缓解记忆退化以及让多个智能体并行工作尤其有帮助。

通过将定理声明与证明分别放入不同文件，并独立维护它们之间的关联，加快了 Lean 编译速度并最大限度减少了资源消耗。

通过为每个定理声明维护自然语言描述，实现搜索与复用，从而得到更简洁的证明路径。

来自 Prove2Me 计划的关键里程碑，Claude 正是依据该计划来形式化费马大定理。三个彩色区块对应 Claude 在通往最终目标过程中必须证明的三个核心子定理。该图紧密遵循了 Wiles 的原始证明。

借助 Prove2Me 和基于 Claude Code 的多智能体框架，一个智能体团队在不到两周的时间内完成了证明，消耗了约 60 亿个输出 token，这些 token 来自一个与 Claude Fable 5.1 大致相当的通用的内部研究模型。完成的证明已通过 Lean 校验；它仅使用了 Lean 的三个标准公理，并且一个比较器确认该定理的声明与 Mathlib 中费马大定理的声明一致。

减轻形式化验证的负担

我们能够以如此之快的速度完成这一证明，表明如今对数学的大片领域进行形式化已成为可能。这既能发现数学证明通用体系中可能存在的错误，也能减轻同行评审新成果的负担。在审阅了 Claude 的 Lean 证明后，Kevin Buzzard 对我们说：

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

形式化也是人类对 AI 生成的数学结果建立信心的一个关键因素。随着 AI 及 AI 辅助的数学家以前所未有的速度产出更多（声称的）证明，AI 辅助的形式化能够分担人类评审者的一部分工作。我们预计，未来在为人类读者撰写任何文稿的同时，配套产出一份形式化证明将成为常态。尽管我们认为形式化证明不应取代人类可理解的论述，但它可能是数学界跟上 AI 生成成果步伐的唯一可行途径。

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

形式化费马大定理（FLT）是一个 token 密集型项目，但它也是有史以来构建的最大规模 Lean 证明。Anthropic 研究人员用三个个人版 Claude Max 订阅做了一项小实验，用于形式化 Hardy-Littlewood 圆法的应用。智能体完全通过 Prove2Me 协作，在短短三天内共同完成了维诺格拉多夫三素数定理的形式化。我们认为，只要有合适的脚手架，用消费级 AI 订阅协作形式化重大定理是可以实现的。

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

随着 AI 迅速改变数学研究的面貌，Anthropic 及其他地方的数学家们正在思考这对他们的工作意味着什么。然而，形式化是我们对 AI 的作用感到毫无保留地看好的领域。随着形式化成为一种更常见的工具，我们希望它将有助于维护对数学知识共同体的信任。

致谢

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

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

了解更多

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

推荐阅读材料

《代码中的证明》是一本近期出版的著作，讲述了 Lean 定理证明器的发展历史以及数学形式化的历程。

1996 年的 BBC 纪录片《费马大定理》采访了怀尔斯及其他参与证明的数学家，本文的几位作者对它记忆犹新。

对于具有数学背景的读者，关于“命题即类型”（证明助手如 Lean、Rocq 和 Agda 的底层学科）的技术性历史，可参阅 Philip Wadler 所著的《Propositions as Types》。

Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me：一个用于规模化数学形式化的开放协作平台. arXiv. https://doi.org/10.48550/arXiv.2608.28433

《自动化数学》，Adam Marblestone，发表于《Asterisk》杂志。

脚注

在本科期间，Peng 的科研导师想把 Peng 论文中的成果收录进一篇 Nature 文章。导师问他是否确定证明是正确的。Peng 诚实地回答：“我有 99% 的把握，但这么长的证明很难做到 100% 确定。”Peng 因此错失了在 Nature 上发表成果的机会。

数学界在验证方面遇到困难的例子还有很多。其中最著名的当属 Thomas Hales 于 1998 年对开普勒猜想的证明，该证明经过四年审查，最终由 12 位审稿人组成的评审组以“99% 确定”收尾（Hales 最终领导了一个二十人的项目 Flyspeck，将该证明形式化）。Grigori Perelman 于 2002 年对庞加莱猜想的证明，数学界花了大约四年时间、通过三份各约 300 页的阐述才得以接受。Harald Helfgott 于 2013 年对弱哥德巴赫猜想的证明至今仍在审查中。有时，后来被证明是错误的结论会被接受多年，其他数学家便在这些错误的基础上构建自己的理论。

这部分是因为 Mathlib 简洁且经过充分审阅，而我们的证明很可能比实际需要的要冗长得多。