Anthropic's Claude Formalizes Proof of Fermat's Last Theorem in Lean

Anthropic announced that its Claude model has become the first AI system to produce a complete, computer-verifiable proof of Fermat's Last Theorem in the formal language Lean. The process, described as largely autonomous, took 11 days and produced the largest proof file of its kind to date.

What Claude Actually Did

The task was not to devise a new proof, but to translate existing mathematical reasoning into a formal notation that a computer can verify step by step, with no gaps and no reliance on trust. Fermat's Last Theorem, first stated in the 17th century and not proved until 1995 by Andrew Wiles, has for decades been considered one of the hardest candidates for full formalization because of the length and complexity of the original argument.

Claude worked across dozens of parallel agents, using the Prove2Me platform, which maintains a dependency graph between theorems and lets individual model instances share already-proved fragments instead of proving them from scratch. According to Anthropic, an initial attempt without access to this tool failed, and the breakthrough came only after integration with Peng's system.

The Human Role

Anthropic stresses that human involvement was limited to occasional high-level guidance. Tianyi Peng reportedly steered the model's attention with short notes, such as prioritizing the Jacobian criterion or speeding up work on the Mazur theorem, without intervening in the details of the proof itself.

In the model's published reasoning trace, Claude at one point noted the completion of a key stage with a brief remark in English, suggesting the system itself recognized the significance of the moment. About 7 percent of the code lines without ready-made templates come from failed agent attempts that ultimately did not make it into the final proof but were preserved in the work log.

Assessment From the Math Community

Kevin Buzzard of Imperial College London, who has led a community project formalizing Fermat's Last Theorem in Lean for years, reviewed the resulting artifact. His assessment, quoted by Anthropic, is cautiously enthusiastic: the proof assumes nothing beyond the axioms of mathematics, and the autoformalization technique itself touched on algebra, harmonic analysis, geometry, and number theory along the way.

This is a remarkable feat of autoformalization which, according to the Anthropic researchers, took only 11 days, and proves Fermat's Last Theorem with no assumptions beyond the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry, and number theory, and we learn that AI autoformalization artifacts are now robust enough to build on - Kevin Buzzard, Imperial College London

If automatic formalization of FLT is now possible, we've taken a big step toward automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools that catch errors in the current mathematical corpus and take work off the shoulders of reviewers - Kevin Buzzard, Imperial College London

What This Means in Practice

Formalizing a result in Lean is not the same as discovering a new theorem. Claude did not find a new proof path; it rewrote Wiles's existing argument, in the version later refined by Darmon, Diamond, and Taylor, into a language a machine can verify with no interpretive uncertainty. That distinction matters, since it separates this achievement from claims about AI "creating new mathematics."

Buzzard nonetheless points to the practical value of such tools: rigorously checking proofs generated by language models is today typically a very costly process carried out by hand by humans. Systems capable of autoformalization at this scale could eventually verify mathematical claims produced by other AI models automatically, instead of leaving that work to human reviewers.

For the formal mathematics verification community, it is a sign that a scale previously reached only by multi-year community projects is now within reach of a single AI model run lasting under two weeks. The Mathlib library itself, built collectively over years, remains smaller than the proof Claude generated for this single theorem.

Cost and Limitations

The project consumed roughly 6 billion tokens generated by a model comparable in power to Claude Fable 5.1, making it a very computationally expensive research experiment rather than a production-ready, repeatable process. Anthropic did not disclose an exact dollar cost, but the scale of token usage suggests spending in the tens of thousands of dollars for a single run.

The company also notes that part of the code, about 7 percent of lines without ready-made templates, came from failed agent attempts and was not fully cleaned of trial-and-error artifacts. Even so, the mere fact that such a large formal proof compiled and passed verification at all is regarded in the field as evidence the method has matured, not just a technical curiosity.