Fermat's Last Theorem is published by General Action, the company that makes Emdash. When we recommend Emdash, we are recommending our own product. About this site
Formalizing Fermat's Last Theorem in Lean
As of November 13, 2026, Fermat’s Last Theorem has a complete, computer-checked proof in the Lean theorem prover. It was announced by Anthropic on September 4, 2026, and was written by AI agents in 11 days. The human-led project that set out to do this, directed by Kevin Buzzard at Imperial College London and funded until September 2029, is continuing with a different aim: a modern proof that people can read and build on.
Everything on this page was checked against the projects’ own pages on November 13, 2026. This is a fast-moving subject, so follow the links for the current state.
What formalization means
Section titled “What formalization means”A published proof is written for people. It skips routine steps, cites other papers and trusts the reader to fill gaps. A formal proof is written in a programming language whose rules are the rules of logic. A small program, the kernel, checks every inference. If the file compiles, the theorem follows from the axioms.
Lean describes itself as “an open-source programming language and proof assistant”. Its community library, Mathlib, holds the definitions and theorems that new work builds on. Buzzard put its size at 2.3 million lines in July 2026, written over nine years.
The statement of Fermat’s Last Theorem is short in Lean. This is the one in Anthropic’s repository:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ nThe hypotheses 0 < a, 0 < b, 0 < c matter. Lean’s natural numbers include zero, and Buzzard points out that a version without them is simply false, since 03 + 03 = 03. Getting the statement right is a separate task from proving it.
The difficulty is everything beneath that one line. The proof uses elliptic curves, modular forms and Galois representations, and in 2023 many of those objects had never been defined in any proof assistant. Fermat’s Last Theorem was the last unformalized entry on Freek Wiedijk’s list of 100 theorems, a long-standing benchmark for the field.
The Imperial College London project
Section titled “The Imperial College London project”The FLT project describes itself as an “ongoing multi-author open source project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover”. From its own pages:
- Lead: Kevin Buzzard. Host: Imperial College London.
- Funding: grant EP/Y022904/1 from the Engineering and Physical Sciences Research Council (EPSRC), running until September 2029. Buzzard has described it as £1M over five years. The project notes say the grant took effect in October 2024.
- Proof route: not the original 1995 argument. It is “a modern variant of the original Wiles/Taylor-Wiles proof, borrowing heavily from the ideas of Khare and Wintenberger”, planned by Richard Taylor in discussions with Buzzard.
- First goal: to reduce Fermat’s Last Theorem to results that “were known by the end of the 1980s”, and to state those results in Lean.
- Method: a public blueprint that breaks the proof into small lemmas contributors can claim, with reusable material sent upstream to Mathlib.
- Repository: created in November 2023, Apache-2.0 licensed. On November 13, 2026, GitHub showed about 1,700 commits from roughly 70 contributors, the most recent push two days earlier.
A related community project had already finished one historical milestone: Kummer’s theorem for regular primes was formalized in Lean and published in 2025.
The first complete proof: September 2026
Section titled “The first complete proof: September 2026”On September 4, 2026, Anthropic announced what it called “the first complete computer-checked proof of Fermat’s Last Theorem”. The facts below are from that post and the repository.
| Aspect | What was reported |
|---|---|
| Who wrote the Lean code | Dozens of Claude AI agents, running what the post calls “a general-purpose internal research model” |
| Tooling | Prove2Me, a collaborative formalization platform from Tianyi Peng’s group at Columbia University, and a multi-agent harness based on Claude Code |
| Time taken | 11 days, “largely autonomously” |
| Size | About 13 million lines of Lean and 29,500 intermediate theorems in the final proof |
| Proof route | The Wiles and Taylor–Wiles argument as set out by Darmon, Diamond and Taylor |
| Human input | Limited to “occasional high-level instructions” from Tianyi Peng, the researcher who directed the run |
| Built on | Mathlib, the Imperial College FLT project and the flt-regular project |
| Axioms | Lean’s three standard axioms only |
| Licence and upkeep | Apache-2.0. The repository is labelled a research artifact that is not maintained and does not accept contributions |
Anthropic’s post is open about the rough edges. Early attempts failed because the agents “lost track of the project’s state”. The run consumed about six billion output tokens. And the result, in its words, “is likely much longer than it needs to be”.
What Kevin Buzzard said
Section titled “What Kevin Buzzard said”Anthropic asked Buzzard to review the code. His account is the most useful single source on what the result means.
- It is correct. “I’ve compiled the code base and run comparator on it — it checks out.” He needed a 96-core machine with 500 GB of memory to do so, which Anthropic lent him.
- It is the old proof. The formalization follows the 1995 exposition, “not the modern proof which I have been formalizing myself”.
- It adds no mathematics. In his words, “mathematically this work of anthropic tells us essentially nothing”. Buzzard says he was already 99.9% sure the proof of the theorem was sound.
- It matters for what it shows about AI. If thousands of pages can be formalized in 11 days, he expects “formalization of modern research being done on the fly”.
- His project is not finished. He had promised his funder a reduction of the theorem to the 1980s, which this exceeds. He had also promised contributions to Mathlib and “a dynamic document enabling humans to explore the modern proof”. Both remain.
A guest post on his blog in October, which Buzzard wrote with six co-authors, is blunter about the artefact: the accomplishment is impressive, but “this piece of AI-generated code probably has little ongoing value”. Wiedijk’s list now credits the entry for Fermat’s Last Theorem to “Lean, Anthropic”, and shows all 100 theorems formalized in Lean.
How to read “checked in Lean”
Section titled “How to read “checked in Lean””In a post on November 12, 2026, Buzzard set out four questions to ask of any such claim, especially when the code is AI-generated. Applied to this proof:
- Does the Lean statement match the real theorem? Here it is the single declaration shown above. It uses only standard definitions and can be read by eye.
- Does the code compile? Yes, though not on ordinary hardware. The repository reports a build of 5 hours 32 minutes at 96 parallel jobs.
- Does it prove that statement, with no added axioms or redefined symbols? This is what the
comparatortool checks, and Buzzard ran it. - Does it exploit a bug in Lean’s kernel? Kernel bugs are real: Buzzard notes that one was found and fixed in 2026. The defence is to recheck the proof with a second kernel written separately. Anthropic’s repository reports that nanoda, a Lean kernel written separately in Rust, accepted the proof. That run used four small patches of Anthropic’s own, one for progress output and three for speed.
A fifth caution comes from the repository itself. The intermediate theorem names are machine-generated, and “where a name and a statement disagree the statement is what was proved”. The code was written to be checked, not read.
How AI use changed during the project
Section titled “How AI use changed during the project”The project’s own documents record the shift.
- December 2023. Buzzard wrote that the available AI tools “are not really able to help with the formalisation aspect of this task, so most of the work will be done by humans”.
- May 2026. Announcing a workshop on the project, he judged that autoformalization “still does not seem to be capable of reliably autonomously formalizing definitions correctly”.
- July 2026. He reported that his PhD student Andrew Yang, using two commercial AI models, had written 250,000 lines of Lean in about two weeks that “basically completely finished” the formalization of a modularity lifting theorem needed for the project.
- September 2026. The complete proof described above.
Two cautions keep this in proportion. The work was translation of known mathematics, not discovery. And Anthropic’s own post says it does not think “a formalized proof should replace a human-understandable exposition”.
Where things stand
Section titled “Where things stand”| Effort | Proof route | Status on November 13, 2026 |
|---|---|---|
| Imperial College FLT project (Buzzard) | Modern proof, after Khare–Wintenberger and others | Ongoing. Funded to September 2029 |
| flt-regular | Kummer’s theorem for regular primes | Complete. Published 2025 |
| Anthropic’s formalization | Wiles and Taylor–Wiles, via Darmon–Diamond–Taylor | Complete. Released September 2026, not maintained |
For the mathematics being formalized, see How Wiles proved it. For Kummer’s theorem, see The statement and small cases.
Frequently asked questions
Has Fermat's Last Theorem been formalized in Lean?
Yes. On September 4, 2026, Anthropic announced a complete proof of Fermat's Last Theorem in Lean 4, produced by its AI system in 11 days. Kevin Buzzard of Imperial College London compiled the code and confirmed that it proves the theorem from Lean's standard axioms. His own project, which formalizes a more modern proof, is still under way.
What does it mean to formalize a proof?
Formalizing a proof means rewriting it in the language of a proof assistant such as Lean, with every step spelled out, so that a small trusted program called the kernel can check each inference mechanically. Nothing is left to the reader, including steps a human author would call obvious.
Who leads the Fermat's Last Theorem project at Imperial College London?
Kevin Buzzard, a professor at Imperial College London. The project is funded until September 2029 by grant EP/Y022904/1 from the UK's Engineering and Physical Sciences Research Council. The proof route was planned by Richard Taylor in discussions with Buzzard.
Does the Lean proof show anything new about Fermat's Last Theorem?
Not mathematically. Buzzard wrote that the formalization tells us essentially nothing new, because number theorists were already confident in the proof. What it demonstrates is that thousands of pages of advanced mathematics can now be translated into machine-checkable form by AI systems.
Can a proof checked in Lean still be wrong?
The proof itself is very unlikely to be wrong, but the claim around it can be. The Lean statement might not say what the English statement says, the code might add an axiom, or it might exploit a bug in the checker. Buzzard lists four checks to rule these out, and the checks have a cost of their own for a proof of 13 million lines.