形式化也是人类如何建立对 AI 生成数学结果之信心的一个主要因素。随着 AI 以及有 AI 辅助的数学家产出比以往任何时候都多的（所谓的）证明，AI 辅助的形式化能替人类审阅者卸下一部分负担。我们预计，在任何面向人类读者的成稿之外一并产出一份形式化证明，将会变得普遍。尽管我们并不认为形式化证明应当取代人类可读的论述，但它可能是数学界跟上 AI 生成成果的唯一可行方式。
写 Lean 似乎也有助于 Claude 证明新结果。我们近期由 Claude 完成的许多结果，都是在证明的同时并行做形式化的；Claude 似乎会用这些局部证明来独立检验自己的假设，就像它写数值模拟来确认自己方向没走偏一样。
形式化 FLT 是一个 token 消耗巨大的项目，但它同时也是有史以来构建出的最大规模的 Lean 证明。Anthropic 的研究人员做了一个小实验：用三个个人 Claude Max 订阅来形式化 Hardy-Littlewood 圆法的若干应用。智能体们完全通过 Prove2Me 协作，仅用三天就共同完成了 Vinogradov 三素数定理的形式化。我们认为，只要有合适的支撑框架，用消费级 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 和其他参与该证明的数学家，本文的一些作者对它记忆犹新。
- 对有数学背景的读者，命题即类型（propositions-as-types，是 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
Claude moved the proof of Fermat's Last Theorem into Lean in 11 days. Not new math: checking a proof went from years to two weeks.
Indigo's conclusion
The biggest AI milestone yet in checking math. It doesn't overturn “verification can't be skipped”; it draws the line: where a field has a cheap machine judge like Lean, checking drops from years to two weeks; where it doesn't, it stays slow.
How to read this Anthropic's own release, meant partly to show off Claude, sell “formalization as the trust layer” and recruit research partners. But “a valid Lean proof exists” is confirmed twice, by Lean's machine check and by Kevin Buzzard, so it is hard fact. How fast, how cheap and what it means are the company's own claims; keep the two apart.
What to remember
Formalization, not new math: Claude translated Wiles's existing proof into Lean; it did not prove Fermat again.
Whether checking speeds up depends on a cheap machine judge. Math has Lean and speeds up; wet labs, clinics and physics don't.
The scaffolding made the difference: the model alone lost track and stopped cooperating; Prove2Me's graph of theorems carried it over the line.
“Formalization as trust layer” holds only for math Lean covers. Most frontier math isn't formalized, and empirical science has no Lean at all.
Breakdown · 5 steps
01
The first machine-checked proof of Fermat's Last Theorem
11 days, largely autonomous, 13 million lines of Lean, endorsed by Buzzard, the field's leading expert. Anthropic says it plainly: what's new is the checking, not the math. Read this part →
02
Checking proofs has always been math's bottleneck
Wiles's 129-page proof took months to review; a fatal gap turned up after his first lecture and took a year to fix. The Kepler conjecture took 4 years, and a 12-person panel would only say “99% certain”. Read this part →
03
Agents lost track; the scaffolding saved them
Formalization was expected to take years. Early agents quickly lost the project's state and stopped cooperating; after switching to Prove2Me's graph of theorems, it was done in two weeks. Read this part →
04
Formalization as the trust layer for AI math
AI will produce more math than people can review. Their bet: next to every proof written for people, attach a version a machine can check. Read this part →
05
Thanks, and an admission: the code is far longer than needed
Thanks to the Mathlib community and earlier theory. A footnote admits the 13 million lines are brute force, and a few paragraphs recall proofs that took mathematicians years to check. Read this part →
What it means for Rewired Index
First-hand evidence for the “sell the verification tools” theme: the Lean and Mathlib ecosystem and collaboration platforms like Prove2Me. It points the same way as Pachocki, favoring evaluation and formal-verification tools; but Lean FRO and Prove2Me are not companies, so there are no names to own.
What would change my mind
fields without a machine judge (wet labs, clinics, physical judgment) see checking speed up by a similar amount.
How to read this
Anthropic's own release, meant partly to show off Claude, sell “formalization as the trust layer” and recruit research partners. But “a valid Lean proof exists” is confirmed twice, by Lean's machine check and by Kevin Buzzard, so it is hard fact. How fast, how cheap and what it means are the company's own claims; keep the two apart.
The first machine-checked proof of Fermat's Last Theorem
11 days, largely autonomous, 13 million lines of Lean, endorsed by Buzzard, the field's leading expert. Anthropic says it plainly: what's new is the checking, not the math.
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 Arithmetica that 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 in 1995, 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.
02
Checking proofs has always been math's bottleneck
Wiles's 129-page proof took months to review; a fatal gap turned up after his first lecture and took a year to fix. The Kepler conjecture took 4 years, and a 12-person panel would only say “99% certain”.
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.
03
Agents lost track; the scaffolding saved them
Formalization was expected to take years. Early agents quickly lost the project's state and stopped cooperating; after switching to Prove2Me's graph of theorems, it was done in two weeks.
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
Time progression of FLT formalization.
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.
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 that agents 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.
Key milestones from the Prove2Me plan that Claude used to formalize Fermat’s Last Theorem. The three colored sections correspond to three core sub-theorems that Claude had to prove on the way to its final goal. This graph closely follows Wiles’s original proof.
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.
04
Formalization as the trust layer for AI math
AI will produce more math than people can review. Their bet: next to every proof written for people, attach a version a machine can check.
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.
05
Thanks, and an admission: the code is far longer than needed
Thanks to the Mathlib community and earlier theory. A footnote admits the 13 million lines are brute force, and a few paragraphs recall proofs that took mathematicians years to check.
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 300 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.
- 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 20-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.
Where Indigo landsFurther
Indigo's conclusion
The biggest AI milestone yet in checking math. It doesn't overturn “verification can't be skipped”; it draws the line: where a field has a cheap machine judge like Lean, checking drops from years to two weeks; where it doesn't, it stays slow.
What to remember
Formalization, not new math: Claude translated Wiles's existing proof into Lean; it did not prove Fermat again.
Whether checking speeds up depends on a cheap machine judge. Math has Lean and speeds up; wet labs, clinics and physics don't.
The scaffolding made the difference: the model alone lost track and stopped cooperating; Prove2Me's graph of theorems carried it over the line.
“Formalization as trust layer” holds only for math Lean covers. Most frontier math isn't formalized, and empirical science has no Lean at all.
Back on the long-running theses
confirms
Whether verifiable domains generalize Once again AI's leap lands exactly where a cheap machine judge exists.
adds to
Verification can't be compressed It looks like a counterexample but strengthens the view: whether verification compresses depends on a cheap machine judge.
Jakub Pachocki, An Alien Mind He says monitoring and verification are the bottleneck; this gives the answer for math: formalization as trust layer, only where Lean reaches.
What it means for Rewired Index
First-hand evidence for the “sell the verification tools” theme: the Lean and Mathlib ecosystem and collaboration platforms like Prove2Me. It points the same way as Pachocki, favoring evaluation and formal-verification tools; but Lean FRO and Prove2Me are not companies, so there are no names to own.
What would change my mind
fields without a machine judge (wet labs, clinics, physical judgment) see checking speed up by a similar amount.
Finished. Indigo's take on this piece is in two places: