Fermat's Last Theorem says that xⁿ + yⁿ = zⁿ has no solutions in positive whole numbers when n is greater than 2. Pierre de Fermat scribbled it in a margin in the 1630s; Andrew Wiles proved it in the 1990s with some of the hardest mathematics ever written. On 4 September 2026 Anthropic announced that Claude had, in 11 days, produced the first complete computer-checked version of that proof[1]. This post explains what that means, why it is a computer-science story as much as a maths one, and what it does not mean.
Timeline
- 1630sFermat claims a proof that 'this margin is too narrow to contain'.
- 1994–95Andrew Wiles (with Richard Taylor) completes the proof.
- 2024Kevin Buzzard begins a human-led project at Imperial College London to formalise the proof in Lean.
- Aug 2026Claude agents complete a full Lean formalisation in 11 days.
- 4 Sep 2026Anthropic announces the result; Buzzard reviews it.
What a proof assistant does
GCSE coreA human-written proof leaves small steps to the reader. Even expert referees can miss a gap. A proof assistant such as Lean removes that risk. You write definitions and proofs as code, and a small, trusted checker (the kernel) confirms that every step follows from logic and from earlier results. If the code compiles, the theorem is verified. It is like a compiler that refuses to run your program unless it is provably correct.
A formal proof is a tree: the final theorem rests on big intermediate results, which rest on lemmas, which rest on definitions and basic facts. Lean checks every link. Press the button to check the tree from the foundations up. Schematic; the real tree has about 29,500 theorems.
What Claude actually did
A-Level extension- It formalised a simplified version of Wiles's proof, due to Darmon, Diamond and Taylor[1].
- The result is about 13 million lines of Lean and about 30,300 theorems (around 29,500 used in the final proof), more than five times the size of Mathlib[1].
- Dozens of Claude agents worked in parallel over 11 days, using about six billion output tokens from an internal research model[1].
- Human mathematical input was limited to occasional high-level instructions from Anthropic researcher Tianyi Peng[1].
- The proof relies only on Lean's three standard axioms, and a comparator confirmed that the final theorem states exactly what Mathlib's own statement of Fermat's Last Theorem says[1].
- It reused pieces from Kevin Buzzard's FLT project at Imperial College London, and Buzzard reviewed the finished proof[1].
Quick check
What does it mean that the proof 'compiles' in Lean?
Why checking the statement matters
A computer-checked proof is only useful if it proves the right statement. If the theorem were written slightly wrongly in Lean, a perfect proof of the wrong thing would be worthless. That is why the team used a comparator to confirm the statement matches Mathlib's independently written version, and why the “no extra axioms” check matters: it shows nothing was simply assumed[1]. Verification of the steps and validation of the specification are two separate jobs, exactly as in software testing.
The distinction students often miss
Correct is not the same as elegant (or new).
Exam-style question
Explain the difference between verification and validation, using the formal proof of Fermat's Last Theorem as an example. [4 marks]
Show model answer and mark breakdown
- verification checks that the product is built correctly, i.e. it meets its specification (1 mark)
- here, Lean verifies that every step of the proof is logically correct (1 mark)
- validation checks that the right product was built, i.e. the specification matches what was actually needed (1 mark)
- here, comparing the Lean statement with Mathlib's independent statement of FLT checks that the proof proves the intended theorem (1 mark)
Examiner focus: define both terms and attach each to a specific part of the example.
Common mistake: treating the two words as synonyms. A program can pass every verification check and still do the wrong thing.
Logic, proof and testing connect A-Level maths and computer science. Our Can AI actually do maths? post looks at the wider picture, and the Millennium Prize Problems show which questions are still open.
Sources and further reading
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — scale, agents, axioms, human input, Buzzard review, caveats
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — news coverage
- Lean community: Mathlib — the Lean maths library
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — the human-led project
Last reviewed: 5 October 2026. Figures are typical published values and rules can change. Exam wording varies by specification, so check yours.
Frequently asked questions
Did AI prove Fermat's Last Theorem?
No: Andrew Wiles proved it in the 1990s. What happened in 2026 is that Claude agents translated a version of that proof into Lean, a programming language whose checker verifies every single logical step. The result, announced by Anthropic on 4 September 2026, is the first complete, computer-checked proof of the theorem.
What is Lean?
A proof assistant: a programming language in which definitions, theorems and proofs are written as code. A small trusted program, the kernel, checks that every step follows from the rules of logic and earlier results. If the proof compiles, the theorem is verified, assuming only the axioms built into Lean.
How big was the proof?
About 13 million lines of Lean code and around 30,000 theorems (about 29,500 used in the final proof), more than five times the size of Mathlib, Lean's main community maths library. It took 11 days, with dozens of Claude agents working in parallel and occasional high-level guidance from Anthropic researcher Tianyi Peng.
Is the AI-written proof any good?
It is correct in the sense that Lean has checked it, and Kevin Buzzard, who leads the human-led FLT formalisation project at Imperial College London, reviewed it. But Anthropic says it is likely much longer than it needs to be, and failed attempts left behind about 7% of its non-boilerplate lines. Correct and elegant are different things.
Reader ratings & reviews
Rate this article across a few different things — your rating helps other readers, and helps us improve.
Was this article helpful?
Tell us what you think — a correction, a question it left unanswered, or a topic you'd like covered next.
Prefer To Talk? Book a free video call at a time that suits you: 15 minutes for a quick question, 30 for anything else. Times show in your own time zone.
About the author
Sudershan Soni
Founder & Lead Tutor at Mostak Services — an MSc-qualified Mathematics, Science, Computer Science & STEM tutor with 20+ years of professional experience, teaching students from 11+ and GCSE to A-Level and beyond, online worldwide.
Read full profile