{"id":23793,"date":"2026-09-08T02:12:15","date_gmt":"2026-09-08T02:12:15","guid":{"rendered":"https:\/\/scannn.com\/formalizing-fermats-last-theorem-anthropic\/"},"modified":"2026-09-08T02:12:15","modified_gmt":"2026-09-08T02:12:15","slug":"formalizing-fermats-last-theorem-anthropic","status":"publish","type":"post","link":"https:\/\/scannn.com\/lv\/formalizing-fermats-last-theorem-anthropic\/","title":{"rendered":"Formalizing Fermat's Last Theorem \\ Anthropic"},"content":{"rendered":"\n
\n

We are sharing the first complete computer-checked proof of Fermat\u2019s 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.<\/em><\/p>\n

Around 1637, Pierre de Fermat jotted down a claim in the margin of his copy of Diophantus\u2019s Arithmetica <\/em>that would become one of the most famous mathematical conjectures of all time: no positive integers a, b, c satisfy a\u207f + b\u207f = c\u207f for any n > 2. Fermat\u2019s Last Theorem<\/a> (FLT), as the conjecture became known, turned out to be incredibly difficult to prove. The first proof, from Sir Andrew Wiles in <\/em>1995, ran to 129 pages and required months of painstaking work to verify.<\/p>\n

A decade later, Dutch computer scientist Jan Bergstra proposed \u201cformalizing\u201d Wiles\u2019s 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<\/a> using the Lean proof assistant<\/a>.<\/p>\n

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<\/sup> 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.<\/p>\n

We shared the resulting proof<\/a> with Kevin Buzzard, who said:<\/p>\n

This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat\u2019s 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.<\/p><\/blockquote>\n

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.<\/p>\n

The challenge of verifying mathematical proofs<\/h2>\n

Unlike recent AI-driven<\/a> work on the Riemann hypothesis, which produced novel mathematics<\/em>, what\u2019s novel here is the verification<\/em>\u2014checking 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.<\/p>\n

Fermat\u2019s Last Theorem is an illustrative example.2<\/sup> Fermat wrote down the theorem\u2019s statement in the margin of a book, alongside a tantalizing note:<\/p>\n

I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.<\/p><\/blockquote>\n

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\u20132 million dollars today) was announced for anyone who could produce a correct proof, and 621 incorrect<\/em> attempts were produced in the first year alone.<\/p>\n

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\u2019d discarded earlier could fix the proof. <\/p>\n

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\u2019s own original \u201cmarvelous proof\u201d was incorrect<\/a>.<\/p>\n

Formalizing Fermat\u2019s Last Theorem<\/h2>\n

One way to check a proof\u2019s 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\u2019s been formalized already.<\/p>\n

For FLT, the formalization process was expected to take years. Just the blueprint<\/a> the mathematical community has been using to describe the initial phase of the project runs to 86 pages.<\/p>\n

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\u2019s proof is over 5x the size of Mathlib, the principal community library of mathematical proofs this theorem builds on.3<\/sup><\/p>\n

\n

Time progression of FLT formalization.<\/em><\/figcaption><\/figure>\n<\/p>\n<\/div>\n

Claude\u2019s proof follows a simplified version of Wiles\u2019s proof from Darmon, Diamond, and Taylor<\/a>. Mathematical input from humans was limited to occasional high-level instructions from Tianyi: \u201cJacobian as a scheme sounds high priority,\u201d \u201cpush [the] Mazur [theorem] to be done soon.\u201d You can find excerpts of Claude\u2019s thinking here<\/a>.<\/p>\n

\n
\n
\u201cTHE FLT root reads Proved on the site. Historic moment (modulo re-check).\u201d\n\n\u201c!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me.\u201d\n\n\u201cThe FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.\u201d\n<\/code><\/pre>\n<\/div>\n<\/div>\n
Excerpts of Claude\u2019s thinking as it realizes what it has just accomplished.<\/em><\/p>\n
A number of Claude\u2019s initial attempts failed: while agents had some early success, they quickly lost track of the project\u2019s state and stopped collaborating effectively. Their failed efforts contributed ~7% of the non-boilerplate lines in the final proof.<\/p>\n
The effort succeeded when we switched to using Prove2Me<\/a>, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University. Prove2Me helped by:<\/p>\n
    \n
  1. Maintaining a directed acyclic graph (DAG) of theorem statements<\/strong> that <\/strong>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.<\/li>\n
  2. Speeding up Lean compilation and minimizing resource consumption<\/strong> by separating theorem statements and proofs into different files, with the links between them maintained independently.<\/li>\n
  3. Enabling search and reuse <\/strong>by maintaining a natural-language description of each theorem statement, resulting in a simpler proof path.<\/li>\n<\/ol>\n
    \n
    Key milestones from the Prove2Me plan that Claude used to formalize Fermat\u2019s 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\u2019s original proof.<\/em><\/figcaption><\/figure>\n<\/div>\n
    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\u2019s three standard axioms, and a comparator<\/a> confirmed that the theorem\u2019s statement matches Mathlib\u2019s own statement of FLT.<\/p>\n
    Reducing the burden of formal verification<\/h2>\n
    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\u2019s Lean proof, Kevin Buzzard told us:<\/p>\n
    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.<\/p><\/blockquote>\n
    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.<\/p>\n
    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\u2019s on the right track.<\/p>\n
    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\u2019s Three Primes Theorem<\/a> in just three days. We think with the right scaffold, collaborative formalization of major results with consumer AI subscriptions is achievable.<\/p>\n
    To this end, Anthropic<\/a> as well as other labs<\/a> have recently expanded their support for external researchers\u2014including mathematicians working on pure math and formalization\u2014with free and discounted subscriptions and research credits. We also offer dedicated grants<\/a> for larger scientific projects, which could include formalizing other major theorems or improving Lean or Mathlib.<\/p>\n
    With AI rapidly changing what it looks like to do math research, mathematicians\u2014at Anthropic and elsewhere\u2014are grappling with what that means for their work<\/a>. 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.<\/p>\n
    Acknowledgments<\/h2>\n
    Our formalization effort is a small piece of the long history of Fermat\u2019s 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\u00e9 Weil, among others. Claude\u2019s proof follows the exposition by Henri Darmon, Fred Diamond, and Richard Taylor.<\/a><\/p>\n
    Our proof adapts pieces from the Imperial College London FLT project<\/a> led by Kevin Buzzard and the flt-regular project<\/a>. Lean and Mathlib are both their own labors of love and have received contributions from hundreds of mathematicians, many working with the Lean FRO<\/a>. We thank Kevin Buzzard for reviewing the proof and for his comments.<\/p>\n
    Learn more<\/h2>\n
    The full proof is available on GitHub<\/a> along with a written walk-through of the proof.<\/p>\n
    Recommended expository reading<\/h3>\n