Anthropic's Claude AI completes machine-verified proof of Fermat's Last Theorem in 11 days

Anthropic said this week that its Claude artificial intelligence system had produced the first complete, computer-verified formalization of Fermat's Last Theorem, a problem that sat unsolved for 358 years before the British mathematician Andrew Wiles cracked it in 1995. According to a research report the company published on its site, dozens of Claude agents worked largely autonomously for 11 days to translate Wiles's proof into the Lean 4 programming language, a system mathematicians use to check arguments with the same rigor a compiler applies to software.

The distinction between a mathematical proof and a formalized one matters to specialists. Wiles's original argument, along with the work of Richard Taylor that repaired a gap in it, was accepted by the mathematical community through years of expert peer review. A Lean formalization instead lets a computer verify every logical step mechanically, removing any reliance on human readers catching an error. Anthropic says the resulting proof was checked by Lean's own compiler and cross-verified with two independent kernel checkers, and that it rests on nothing but Lean's three standard axioms, with no placeholder steps or shortcuts. The full formalization, along with a written walk-through, is posted on a public GitHub repository under an Apache 2.0 license.

Thirteen million lines, thirty thousand theorems

The scale of the undertaking is what has drawn attention beyond Anthropic's usual audience of AI researchers. The finished formalization runs to roughly 13 million lines of Lean code, more than five times the size of Mathlib, the community-maintained library that underpins most formal mathematics done in Lean today. Along the way, the Claude agents proved about 30,300 intermediate theorems, of which 29,500 were ultimately used in the final proof; the rest were dead ends the system discarded. Anthropic says the run consumed roughly 6 billion output tokens from an internal research model comparable in capability to a Claude Fable-class system, and that the human mathematician overseeing the project, an Anthropic researcher named Tianyi Peng, contributed little beyond occasional one-line hints about which parts of the proof to prioritize.

The agents did not work in isolation. They coordinated through Prove2Me, an open platform Peng designed with collaborators at Columbia University and described in a paper posted to the arXiv preprint server. The system maintains a directed graph of theorem statements that lets many agents work on different branches of a proof at once without losing track of what still needs to be shown, a problem that Anthropic said had caused earlier, smaller-scale attempts to stall as individual agents lost sight of the larger argument. Separating theorem statements from their proofs into different files also sped up compilation and let agents reuse work rather than duplicate it.

A theorem four centuries in the making

Fermat's Last Theorem states that no three positive whole numbers a, b and c can satisfy the equation a^n + b^n = c^n for any integer value of n greater than two. Pierre de Fermat scribbled a claim in 1637 that he had found a proof too large to fit in the margin of a book, but none was ever found among his papers, and the statement went unproven for centuries despite drawing some of the era's best mathematicians. Wiles, working largely in secret at Princeton University, announced a proof in 1993 that was found to contain a gap; he and Taylor closed it the following year, and the corrected argument was published in 1995, running to roughly 129 pages of dense algebraic geometry.

Turning that proof into a form a machine can verify has been a goal of the formal-mathematics community for years. Kevin Buzzard, a professor of pure mathematics at Imperial College London, has led a community effort to formalize Fermat's Last Theorem in Lean since 2024, backed by a five-year grant from Britain's Engineering and Physical Sciences Research Council. That project, built by human volunteers working through Mathlib, has been expected to take years to complete. Anthropic's Claude system, by contrast, produced its own end-to-end formalization, built on a simplified modern exposition of the argument rather than Wiles's original text, in less than two weeks.

What mathematicians make of it

Buzzard reviewed Anthropic's formalization and was quoted in the company's own research report.

"This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," Buzzard said.

The reaction reflects a broader shift underway in mathematics departments, where formal verification tools that were once a niche interest are increasingly seen as necessary infrastructure. As AI systems generate more mathematical claims and proof sketches, Anthropic argues in its report, formal checkers like Lean will be needed to catch errors quickly and preserve confidence in the shared body of mathematical knowledge, rather than leaving verification to overworked human referees. That argument has particular resonance for Mathlib's maintainers, whose library, built up over more than a decade by volunteer contributors, has now been dwarfed several times over by a single machine-generated artifact.

An artifact, not a finished tool

Anthropic has been careful to frame the result narrowly. The GitHub repository is explicitly labeled a research artifact that will not be maintained going forward, and the company acknowledges the formalization is "likely much longer than it needs to be," since the agents were not optimizing for elegance or brevity, only for a verifiable result. Roughly 7 percent of the non-boilerplate code in the final proof came from earlier attempts that failed and had to be reworked, a reminder that the process, while largely autonomous, was neither clean nor cheap; six billion tokens of inference from a frontier research model represents a substantial computing bill that Anthropic has not disclosed in dollar terms.

What happens next will likely play out on two tracks. Inside Anthropic, the company has signaled it sees large-scale autoformalization as a proving ground for its models' reasoning abilities and a template for applying similar agent architectures to other unsolved formalization targets. Outside it, mathematicians who have spent years building tools like Mathlib and Lean now face a practical question of how to absorb, audit and build on a 13-million-line artifact produced by machines in a fraction of the time human volunteers had budgeted for the same task. Buzzard's own EPSRC-funded formalization project continues independently, and it remains to be seen whether it will draw on Anthropic's proof, run alongside it as a separate verification effort, or serve as the benchmark against which the machine-generated version is ultimately judged.