Anthropic said on September 4 that its Claude models produced the first complete, computer-checked proof of Fermat's Last Theorem in the Lean proof assistant, working largely autonomously over an 11-day run coordinated on Prove2Me, an open formalization platform built by Tianyi Peng and collaborators at Columbia University.

What was produced

Fermat's Last Theorem — that no three positive integers a, b, c can satisfy a^n + b^n = c^n for any integer n greater than two — was first proved by Andrew Wiles in 1995, but that proof and the vast body of mathematics it depends on had never been translated into a form a computer can automatically verify. Anthropic says Claude's run formalized a simplified version of Wiles's argument, in the variant developed by Henri Darmon, Fred Diamond and Richard Taylor, producing roughly 13 million lines of Lean code and 30,300 intermediate theorems, of which about 29,500 were used in the final proof. The effort consumed on the order of six billion output tokens. By line count, Anthropic says the result is more than five times the size of Mathlib, the community-maintained library of formalized mathematics that the proof builds on. An initial formalization attempt failed before Prove2Me's coordination layer — which tracks a dependency graph of theorem statements and dispatches work across multiple Claude agents — was brought in partway through and enabled the run to complete.

Independent review

Anthropic had the artifact reviewed by Kevin Buzzard, a mathematician at Imperial College London who works on formalizing mathematics in Lean and has for years pushed for exactly this kind of machine-checked formalization of major theorems. Buzzard, writing on his own blog, called the result "an extraordinary autoformalization achievement" and said it suggests that automatic formalization of large swaths of the modern mathematical literature is now a realistic near-term prospect rather than a distant goal.

Why it matters

Formal verification — proving software or mathematics correct via a system that checks every logical step — has long been prohibitively labor-intensive to apply at scale by hand. A frontier model autonomously producing a formalization of this size, checked by an outside expert rather than the lab that built the model, is a concrete data point for how far AI-assisted formal methods have moved in a short time, with implications beyond pure mathematics for any domain — safety-critical software, chip design, cryptographic protocols — where a machine-checkable proof of correctness is the standard that matters. It also lands as labs compete on demonstrations of autonomous, long-horizon agentic work; an 11-day largely unsupervised run is itself notable independent of the mathematical result.