Anthropic researchers asked Claude to help formalize Fermat’s last theorem. Formalization means rewriting a human argument in a language a computer can check line by line. The language used here is Lean, a proof assistant: software that accepts only steps that follow from stated rules. Those rules include a small set of axioms, the starting assumptions of the system. Most published math is still written for people, who skip “obvious” steps. Lean cannot skip them. Only a sliver of existing mathematics already lives in Mathlib, the main shared library of Lean proofs, so a large formalization must rebuild many intermediate results.
In 11 days, working mostly on its own, Claude produced what the company presents as the first complete computer-checked proof. It wrote about 13 million lines of Lean and proved about 30,300 intermediate theorems, of which about 29,500 appear in the final argument.
How the work was organized
Early runs failed when agents lost track of the project and stopped coordinating. About 7 percent of the non-boilerplate lines in the finished file came from those failed tries. The run that finished used Prove2Me, an open platform that keeps a map of theorem statements and what depends on what, so many agents can work in parallel, reuse results, and compile Lean more cheaply. The campaign used about six billion output tokens from an internal research model described as similar to Claude Fable 5.1. Lean accepted the finished proof. A separate checker, called a comparator, confirmed that the statement matches Mathlib’s own wording of the theorem and that only Lean’s three standard axioms were used.
The result is an autoformalization achievement—meaning a machine turned existing mathematics into checkable code. Automatic checking of much of the modern literature may follow, which could catch errors and ease refereeing, including of proofs written by language models. Anthropic stresses that a formal file should not replace an explanation written for people. A smaller follow-up, using ordinary paid Claude accounts, formalized Vinogradov’s three primes theorem in three days. The Lean files are public on GitHub.