Loading page…
The new artifact turns an established proof into code that two Lean kernels can check. Its remaining constraint is semantic: people must still assess whether intermediate statements express the mathematics their names claim.
Listen to this story
An independently checkable Lean artifact now reportedly encodes the established proof of Fermat’s Last Theorem, but its main significance is engineering rather than mathematical discovery. Anthropic’s Claude coordinated dozens of agents through Prove2Me to produce roughly 13 million lines and 29,500 intermediate theorems in 11 days. Lean and an independent Rust kernel accepted the code without extra axioms or placeholders, yet reviewers still cannot easily verify that every lemma means what its name claims.
The formalization reportedly follows the Darmon–Diamond–Taylor exposition of Wiles’s proof, not a new proof of the theorem.
A clean rebuild takes about 5.5 hours on 96 CPU cores, peaks at 153 GB of memory, and needs 15 hours for one-core replay.
About 6 billion output tokens reportedly powered the effort; roughly 7% of non-boilerplate lines came from failed attempts left in the repository.
Anthropic’s Claude reportedly generated an end-to-end Lean 4 formalization of Fermat’s Last Theorem in 11 days, creating a large formal proof that software can mechanically check. That is a meaningful new route to verification, not a new solution to the theorem.
Formalization converts mathematical reasoning into explicit steps a computer can check, including steps that conventional papers leave unstated. This artifact follows an established version of Wiles’s argument through Frey curves, Ribet’s theorem and Taylor-Wiles patching. Kevin Buzzard says it follows the Darmon–Diamond–Taylor exposition rather than the modern proof exposition he is developing.
Dozens of Claude agents coordinated through Prove2Me to define concepts, prove intermediate results and assemble the final proof. The platform used a directed graph of theorem dependencies, separated theorem statements from proofs, and attached natural-language descriptions to help agents find relevant lemmas. The effort reportedly consumed about 6 billion output tokens from an internal research model described as roughly comparable to Claude Fable 5.1.
Lean’s kernel accepted the proof using only its three standard axioms, and nanoda, an independently implemented Lean kernel in Rust, also checked it. The artifact reportedly contains no sorry placeholders, added axioms or native_decide escape hatches. Those checks establish that the formal result follows under the specified rules.
They do not determine whether each intermediate lemma’s name matches its claimed mathematical meaning. Buzzard, who says he compiled the repository and ran Comparator successfully, argues that the work adds essentially no mathematical content—but demonstrates that AI could formalize extensive literature and expose incomplete or implicit arguments.
A smaller Prove2Me experiment reportedly used three Claude Max plans to formalize Vinogradov’s Three Primes Theorem in three days. Buzzard’s own project aims to create a human-explorable document about the modern proof, underscoring that readable explanation remains a separate deliverable from checked code.
Editorial analysis
The strategic signal is that agent infrastructure may be becoming as consequential as the underlying model for long-horizon technical work. Here, a theorem-dependency graph, separated proof files and natural-language descriptions gave dozens of agents a shared structure. A smaller three-day Vinogradov result points in the same direction. That does not make 13 million lines of code a useful mathematical explanation. The next test is whether a similar system can formalize current research while producing artifacts experts can navigate, assess semantically and use in review, rather than merely compile.
Loading discussion...
Be the first to share a perspective or an experience.
Reader comments
Newest comments first. Replies stay oldest first.