Anthropic used an advanced prototype of Claude to turn the proof of Fermat's last theorem into computer-checkable code. The company announced the result on 4 September. The output runs to 13 million lines and was produced in 11 days. Mathematicians had expected the same task to take people about ten years. The work is written in Lean, a language computers can check line by line. Andrew Wiles and Richard Taylor completed the original human proof in 1994. Kevin Buzzard of Imperial College London said such a feat was a fantasy two years ago. Alex Kontorovich of Rutgers University said the result astonished him. Buzzard called it roughly ten times harder than an earlier sphere-packing formalization in February. Daniel Litt of the University of Toronto said anything could probably now be formalized.
What changed
Turning Fermat's last theorem into computer-checkable code was expected to take humans about a decade.
What it unlocks
Machine translation of very complex mathematical arguments into computer-verifiable form.
- 13 million lines of proof code
- 11 days versus 10 years expected
- proof announced 4 September 2026
What you need to act on it
- an advanced prototype of Claude, not a generally available product
Sources