Anthropic said on 4 September 2026 that Claude, working largely autonomously for 11 days, had produced what the company calls the first complete computer-checked proof of Fermat's Last Theorem. The proof is written in Lean, a proof assistant: software that checks each step of a proof.[1]
According to Anthropic, dozens of Claude agents wrote about 13 million lines of Lean and proved some 29,500 intermediate theorems used in the final proof. They ran on an internal model that the company describes as roughly comparable to Claude Fable 5.1. The proof follows Henri Darmon, Fred Diamond and Richard Taylor's simplified version of Andrew Wiles's proof. Anthropic says mathematical input from humans was limited to occasional high-level instructions from its researcher Tianyi Peng. The agents coordinated through Prove2Me, a platform built by Peng's group at Columbia University. The proof also adapts parts of an Imperial College London project, led by Kevin Buzzard, to formalize the theorem as a computer-checked proof.[1]
The proof is on GitHub, and its default build fails unless the theorem rests only on Lean's three standard axioms. According to the README, Lean's kernel, the core program that accepts or rejects proofs, checked every declaration. The comparator tool, it says, confirmed that the proved statement matches a reference statement written with Mathlib, Lean's main mathematics library. A second, independent kernel, nanoda, also accepted the proof when run with patches that Anthropic says leave its typing rules unchanged. The README says these checks establish the final theorem if the kernels and checking tools are trusted. But it adds that no tool can check that each intermediate theorem means what its name suggests. Repeating the checks is demanding. Anthropic's build ran for about five and a half hours at 96 parallel jobs, and its comparator run took nearly 15 hours with a peak of 230 GB of memory.[2]
Buzzard wrote on 4 September that he had compiled the code and run comparator, and that it checks out. He added that the work tells number theorists essentially nothing new mathematically, because they already trusted the proof and the formalization follows its early literature. Its significance, he wrote, lies in what it shows is possible in automated formalization.[3]
Sources
Check or correct this page
Verification record
The digest below shows whether the text you are reading matches the published source. It does not show that the reporting is correct. The build computes it from this page's Markdown source and lists it in the site manifest.
a338281e96003920a7742af7449c063d7763146a9a85f7966a5793edc23db8e8
