形式化费马大定理
2026年9月4日
我们在此分享费马大定理的首个完整计算机验证证明。Claude 在 11 天内基本自主完成了该证明，并使用 Lean 编程语言撰写。下文将介绍形式化的实现方式，并分享这项工作对研究型数学可能意味着的一些思考。约在 1637 年，皮埃尔·德·费马在他那本丢番图《算术》的页边空白处写下了一个论断，这个论断后来成为有史以来最著名的数学猜想之一：对于任何 n > 2，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。费马大定理（FLT），即这一猜想后来为人所知的名字，被证明是极其难以证明的。第一个证明由安德鲁·怀尔斯爵士于 1995 年给出，长达 129 页，并需要数月艰苦细致的核验工作。
十年后，荷兰计算机科学家扬·贝格斯特拉提出“形式化”怀尔斯的证明：即将数学推理转换为计算机可以自动检查的形式。自那时起，数学家们一直在开发对这种复杂证明进行编码所需的方法，其中包括一项由伦敦帝国理工学院的凯文·巴扎德于 2024 年发起的多年社区努力，旨在使用 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 需要看到每一步，无论多么琐碎。人类的证明还建立在数百年的已发表成果之上，而形式化工作只能从已被形式化的那一小部分数学开始。
对于费马大定理（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 后，这项工作取得了成功。Prove2Me 是一个由哥伦比亚大学的 Tianyi Peng 及其合作者设计的开放协作式数学形式化平台。Prove2Me 在以下方面提供了帮助：
- 维护一个定理声明的有向无环图（DAG），智能体利用它来决定接下来应尝试证明哪些定理。这对于缓解记忆退化以及允许多个智能体并行工作尤其有帮助。
- 通过将定理声明和证明分别存放在不同文件中，并独立维护它们之间的关联，从而加速 Lean 编译并最大限度地减少资源消耗。
- 通过为每个定理声明维护自然语言描述来实现搜索和复用，从而得到更简洁的证明路径。
借助 Prove2Me 和一套基于 Claude Code 的多智能体框架，一个智能体团队在不到两周的时间内完成了该证明，消耗了约 60 亿个来自通用内部研究模型的输出 token，该模型大致相当于 Claude Fable 5.1。完成的证明已由 Lean 验证；它仅使用了 Lean 的三个标准公理，且一个比较器确认该定理的陈述与 Mathlib 中费马大定理（FLT）的陈述一致。
减轻形式化验证的负担
我们能够如此迅速地完成这一证明，表明现在对数学的绝大部分领域进行形式化已成为可能，这既可能发现常见数学证明体系中的错误，也能减轻审阅新成果的负担。在审阅了 Claude 的 Lean 证明后，Kevin Buzzard 告诉我们：
如果费马大定理的自动形式化如今已成为可能，那么我们就朝着现代数学文献的自动形式化迈出了一大步。此类自动形式化技术将催生新工具，清除当前数学语料库中的错误，并减轻审稿人的负担。这些技术还将使我们能够严格验证由大语言模型生成的数学内容，而目前这一过程通常需要耗费极高的人力成本。
形式化也是人类对 AI 生成的数学结果建立信心的一个关键因素。随着 AI 和 AI 辅助的数学家以前所未有的速度产出更多（所谓的）证明，AI 辅助的形式化工作分担了人类审稿人的部分负担。我们预计，未来在为人类读者撰写的任何文稿旁边，同时产出一份形式化证明将成为常态。尽管我们认为形式化证明不应取代人类可理解的阐述，但它可能是数学界跟上 AI 生成成果步伐的唯一可行途径。
编写 Lean 代码似乎也能帮助 Claude 证明新的定理。我们近期许多由 Claude 撰写的成果都在证明的同时并行完成了形式化，而 Claude 似乎会利用这些部分证明来独立检验其假设，就像它编写数值模拟来确认自己走在正确轨道上一样。
将费马大定理形式化是一个消耗大量 token 的项目，但它也是有史以来构建的最大规模 Lean 证明。Anthropic 的研究人员做了一项小实验，使用三个个人版 Claude Max 套餐来形式化 Hardy-Littlewood 圆法的应用。这些智能体完全通过 Prove2Me 协作，在短短三天内就共同完成了 Vinogradov 三素数定理的形式化。我们认为，只要搭建合适的脚手架，利用消费级 AI 订阅来协作形式化重大成果是可以实现的。
为此，Anthropic 以及其他实验室最近扩大了对外部研究人员的支持——包括从事纯数学和形式化工作的数学家——提供免费和折扣订阅以及研究积分。我们还为规模更大的科学项目提供专项资助，这些项目可能包括形式化其他重要定理，或改进 Lean 或 Mathlib。
随着 AI 迅速改变数学研究的形态，数学家们——无论是在 Anthropic 还是在其他地方——都在思考这对他们的工作意味着什么。然而，在形式化（formalization）这一领域，我们对 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 纪录片《费马大定理》采访了怀尔斯及其他参与证明的数学家，该片至今仍被本文的一些作者深深怀念。
- 对于具有数学背景的读者，关于“命题即类型”（propositions-as-types，即 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
- 《数学自动化》（Automating Math），Adam Marblestone 著，发表于《Asterisk》杂志。
脚注
- 在彭的本科阶段，他的研究导师希望将彭论文中的成果纳入一篇 Nature 文章。导师问他是否确定证明是正确的。彭诚实的回答是：“我有 99% 的把握，但对于这么长的证明，很难做到 100% 确定。”彭因此错失了让自己的研究发表在 Nature 上的机会。
- 数学界在验证方面挣扎的故事还有很多。其中最著名的当属托马斯·黑尔斯（Thomas Hales）1998 年对开普勒猜想的证明，该证明经过四年的评审，最终由 12 位审稿人组成的评审团勉强给出“99% 确信”的结论（黑尔斯最终领导了一个二十人的项目 Flyspeck，将该证明形式化）。格里戈里·佩雷尔曼（Grigori Perelman）2002 年对庞加莱猜想的证明，数学界花了大约四年时间、通过三篇各 300 页的阐述才予以接受。哈拉尔德·赫尔夫戈特（Harald Helfgott）2013 年对弱哥德巴赫猜想的证明至今仍在评审中。有时，最终被证明是错误的结论会被接受多年，而其他数学家会在这些错误的基础上构建自己的理论。
- 这部分是因为 Mathlib 本身简洁且经过充分评审，而我们的证明很可能比实际需要的冗长得多。
Formalizing Fermat's Last Theorem
Sep 4, 2026
We are sharing the first complete computer-checked proof of Fermat’s Last Theorem. Claude worked largely autonomously over 11 days to write the proof in the Lean programming language. Below, we describe how the formalization was done and share some thoughts about what this work could mean for research mathematics.
Around 1637, Pierre de Fermat jotted down a claim in the margin of his copy of Diophantus’s Arithmeticathat would become one of the most famous mathematical conjectures of all time: no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n > 2. Fermat’s Last Theorem (FLT), as the conjecture became known, turned out to be incredibly difficult to prove. The first proof, from Sir Andrew Wiles in1995, ran to 129 pages and required months of painstaking work to verify.
A decade later, Dutch computer scientist Jan Bergstra proposed “formalizing” Wiles’s proof: converting the mathematical reasoning into a form computers can check automatically. Since then, mathematicians have been developing the methods needed to encode such a complex proof, including a multi-year community effort kicked off in 2024 by Kevin Buzzard at Imperial College London to complete the formalization using the Lean proof assistant.
Recently, Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, set out to test whether Claude could make progress on formalizing FLT.1 The result went further than he expected. In 11 days, working largely autonomously, Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
We shared the resulting proof with Kevin Buzzard, who said:
This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
Automatically formalizing a proof as complex as FLT is a significant step towards a future in which all of mathematics can be readily checked. As AI produces ever more proofs, the ability to easily formalize work can lighten the burden of evaluating new results (a process that can take years). We are hopeful that it will become easier, not harder, to trust the body of knowledge upon which mathematics is built.
The challenge of verifying mathematical proofs
Unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what’s novel here is the verification—checking a mathematical proof as one would check a mathematical computation with a calculator. Proving math theorems requires assembling complex logical chains, and if a single link is broken, everything that follows it might turn out to be false. Understanding a novel result deeply enough to be confident in its correctness can take months, or even years, of work.
Fermat’s Last Theorem is an illustrative example.2 Fermat wrote down the theorem’s statement in the margin of a book, alongside a tantalizing note:
I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.
For over 350 years, generations of mathematicians searched for a proof of FLT, marvelous or otherwise. In 1908, a prize of 100,000 German gold marks (the equivalent of 1–2 million dollars today) was announced for anyone who could produce a correct proof, and 621 incorrect attempts were produced in the first year alone.
In June 1993, Wiles presented what he believed to be the first correct proof of FLT in a three-day series of lectures. Two months into an intensive verification effort by several mathematicians, a reviewer asked Wiles a question that exposed a critical gap. Wiles spent a year trying to fix it, first alone and then with his former student Richard Taylor. He was on the brink of abandoning the project when he finally realized an approach he’d discarded earlier could fix the proof.
Wiles published the first correct proof of FLT in May 1995; it relied on modern mathematical techniques that were far beyond what would have been known to Fermat in 1637. Since an elementary proof has not been found after centuries of trying, the mathematical community now believes Fermat’s own original “marvelous proof” was incorrect.
Formalizing Fermat’s Last Theorem
One way to check a proof’s correctness is to ask a computer to do it. Proof assistants like Lean verify the logic of a proof algorithmically, demonstrating its correctness beyond a doubt. The difficult part for humans is rewriting the proof so Lean can understand it. While a proof written for human readers will skip many obvious steps, Lean needs to see every step, no matter how trivial. Human proofs also build on centuries of published work, while a formalization starts from the tiny fraction of math that’s been formalized already.
For FLT, the formalization process was expected to take years. Just the blueprint the mathematical community has been using to describe the initial phase of the project runs to 86 pages.
Claude completed the proof in 11 days, producing computer-verifiable proofs of 30,300 theorems along the way (using 29,500 in the final proof). Dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and use those theorems to prove ever harder statements. At 13 million lines of Lean code, Claude’s proof is over 5x the size of Mathlib, the principal community library of mathematical proofs this theorem builds on.3
Claude’s proof follows a simplified version of Wiles’s proof from Darmon, Diamond and Taylor. Mathematical input from humans was limited to occasional high-level instructions from Tianyi: “Jacobian as a scheme sounds high priority,” “push [the] Mazur [theorem] to be done soon.” You can find excerpts of Claude’s thinking here.
“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.”
Excerpts of Claude’s thinking as it realizes what it has just accomplished.
A number of Claude’s initial attempts failed: while agents had some early success, they quickly lost track of the project’s state and stopped collaborating effectively. Their failed efforts contributed ~7% of the non-boilerplate lines in the final proof.
The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University. Prove2Me helped by:
- Maintaining a directed acyclic graph (DAG) of theorem statements thatagents used to decide what proofs they should attempt next. This was particularly helpful for mitigating memory degradation and allowing multiple agents to work in parallel.
- Speeding up Lean compilation and minimizing resource consumption by separating theorem statements and proofs into different files, with the links between them maintained independently.
- Enabling search and reuse by maintaining a natural-language description of each theorem statement, resulting in a simpler proof path.
With Prove2Me and a Claude Code-based multi-agent harness, a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1. The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.
Reducing the burden of formal verification
The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. After reviewing Claude’s Lean proof, Kevin Buzzard told us:
If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees. The techniques will also enable us to rigorously check LLM-generated mathematics, which is currently typically an extremely costly human-led process.
Formalization is also a major factor in how humans can gain confidence in AI-generated mathematical results. As AI and AI-assisted mathematicians produce more (purported) proofs than ever before, AI-assisted formalization takes part of the load off human reviewers. We expect it will become common to produce a formalized proof alongside any write-up intended for a human reader. Although we do not think a formalized proof should replace a human-understandable exposition, it may be the only feasible way for the mathematical community to keep up with AI-generated contributions.
Writing Lean also seems to help Claude prove novel results. Many of our recent Claude-authored results have been formalized in parallel with their proofs, and Claude appears to use these partial proofs to independently check its hypotheses much like it writes numerical simulations to check that it’s on the right track.
Formalizing FLT was a token-intensive project, but it is also the largest Lean proof ever constructed. Anthropic researchers did a small experiment using three personal Claude Max plans to formalize applications of the Hardy-Littlewood Circle Method. Collaborating entirely through Prove2Me, the agents jointly completed a formalization of Vinogradov’s Three Primes Theorem in just three days. We think with the right scaffold, collaborative formalization of major results with consumer AI subscriptions is achievable.
To this end, Anthropic as well as other labs have recently expanded their support for external researchers—including mathematicians working on pure math and formalization—with free and discounted subscriptions and research credits. We also offer dedicated grants for larger scientific projects, which could include formalizing other major theorems or improving Lean or Mathlib.
With AI rapidly changing what it looks like to do math research, mathematicians—at Anthropic and elsewhere—are grappling with what that means for their work. Formalization, however, is a place where we feel unambiguously good about the role of AI. As formalization becomes a more commonplace tool, we are hopeful that it will help maintain trust in the common body of mathematical knowledge.
Acknowledgments
Our formalization effort is a small piece of the long history of Fermat’s theorem and the development of formal mathematics. The first full proof from Andrew Wiles together with Richard Taylor was a culmination of more than three hundred years of mathematics, integrating ideas from Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Barry Mazur, Robert Langlands, Jerrold Tunnell, Yutaka Taniyama, Goro Shimura, and André Weil, among others. Claude’s proof follows the exposition by Henri Darmon, Fred Diamond, and Richard Taylor.
Our proof adapts pieces from the Imperial College London FLT project led by Kevin Buzzard and the flt-regular project. Lean and Mathlib are both their own labors of love and have received contributions from hundreds of mathematicians, many working with the Lean FRO. We thank Kevin Buzzard for reviewing the proof and for his comments.
Learn more
The full proof is available on GitHub along with a written walk-through of the proof.
Recommended expository reading
- The Proof in the Code is a recent book about the history of the Lean theorem prover and the formalization of mathematics.
- The 1996 “Fermat’s Last Theorem” BBC documentary has interviews with Wiles and other mathematicians involved in the proof, and is fondly remembered by some authors of this post.
- For those with a mathematical background, a technical history of propositions-as-types (the underlying discipline of proof assistants such as Lean, Rocq, and Agda) can be found in Propositions as Types by Philip Wadler.
- 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, in Asterisk Magazine.
Footnotes
- During his undergrad, Peng’s research advisor wanted to include results from Peng’s thesis in a Nature article. He asked Peng whether he was sure the proof was correct. Peng’s honest answer was: “I'm 99% sure, but it's hard to be 100% certain about a proof this long.” Peng missed out on getting his work published in Nature.
- There are numerous other stories of the mathematical community struggling with verification. Among the most famous is Thomas Hales’s 1998 proof of the Kepler conjecture, which spent four years in review before a 12-referee panel settled for “99% certain” (Hales eventually led a twenty-person project, Flyspeck, that formalized the proof). Grigori Perelman’s 2002 proof of the Poincaré conjecture took the community roughly four years and three 300-page expositions to accept. Harald Helfgott’s 2013 proof of the weak Goldbach conjecture is still under review. Sometimes results that turn out to be wrong are accepted for years, and other mathematicians build their theories on these faulty foundations.
- This is partly because Mathlib is concise and well-reviewed, while our proof is likely much longer than it needs to be.