Loading…
On 4 September 2026 Anthropic announced that Claude had produced the first end-to-end, computer-checked proof of Fermat's Last Theorem in the Lean proof assistant.
A multi-agent Claude system did the work largely autonomously in 11 days, writing about 13 million lines of Lean and proving 30,300 theorems, 29,500 of them used in the final proof.
The proof follows Andrew Wiles's 1995 argument; formalisation does not discover new mathematics but converts an existing proof into a form a computer can verify line by line.
Imperial College London's Kevin Buzzard, who leads the human-run FLT formalisation project begun in 2024, reviewed the result.
Fermat notes the claim in the margin of his copy of Diophantus's Arithmetica, saying the margin is too small for his proof
Gerhard Frey links FLT to elliptic curves; Ken Ribet proves the link, reducing FLT to the modularity conjecture
Andrew Wiles's proof, via the modularity theorem for semistable elliptic curves, is published
Wiles receives the Abel Prize for the proof
Kevin Buzzard begins the human-led project to formalise FLT in Lean
Anthropic announces Claude's complete formal proof in Lean
Writing every step of a proof in a precise computer language so a proof assistant such as Lean can check it mechanically. It finds hidden gaps and removes reliance on human referees, who can take years to check long proofs.
Simple Analogy: Like a spell-checker that checks logic, one step at a time.
GS Paper III > Science and Technology > Artificial Intelligence
General Awareness > Science and Technology / Mathematicians
No positive integers x, y, z satisfy xⁿ + yⁿ = zⁿ for any integer n greater than 2
Open-source proof assistant and programming language used to write machine-checkable proofs
Lean's community-built library of formalised mathematics