Anthropic's Claude agents produce machine-checked Lean 4 proof of Fermat's Last Theorem in 11 days

Anthropic has published a complete Lean 4 formalization of Fermat's Last Theorem: a proof of roughly 13 million lines, written largely by Claude agents over 11 days and accepted by a machine checker rather than human referees. According to a dev.to write-up, the announcement came on September 4, 2026, and Kevin Buzzard, the Imperial College London mathematician who has led a separate human project toward the same goal since 2024, rebuilt the entire artifact and confirmed that it compiles.

The proof and how it was checked

Fermat's Last Theorem states that no positive integers a, b and c satisfy a to the n plus b to the n equals c to the n for any integer n greater than 2. Andrew Wiles's proof, completed with Richard Taylor after a gap was found in his 1993 announcement, was published in May 1995 across 129 pages. Formalizing it in Lean means rewriting the argument as code so detailed that the proof assistant's kernel rejects any missing step.

The repository makes its trust base explicit: a one-line theorem statement, plus a build-time check that the proof depends on exactly Lean's three standard axioms — propext, Classical.choice and Quot.sound — with no sorry placeholders and no native_decide escapes into compiled code outside the kernel.

The dev.to report lists the verification numbers: a from-scratch build took 5 hours 32 minutes across 96 parallel jobs, peaking at 153 GB of RAM; a comparator replay took 14 hours 46 minutes at 230 GB; and nanoda, an independent Rust implementation of the Lean kernel, checked 1,052,234 declarations without errors. The code spans 60,475 modules under Lean 4.33.1. Readability was deliberately sacrificed: the README states that theorem names are machine-generated and that the artifact is written to be checked rather than read, and it is offered as an unmaintained research output.

How the agents worked

Anthropic's research post, as described by dev.to, involved dozens of Claude agents running in a Claude Code multi-agent harness on Prove2Me, a platform built by Tianyi Peng of Columbia. Prove2Me maintains a directed acyclic graph of theorem statements with Fermat's Last Theorem at the root, so every agent can see which lemmas are proved and which are still open. The model is described as a general-purpose internal research model roughly comparable to Claude Fable 5.1.

The shared graph was a late addition. Early runs collapsed because agents lost track of the project's state and stopped cooperating, though those attempts still contributed about 7 percent of the non-boilerplate lines. Human input was limited to occasional high-level direction from Peng. The agents worked from the 1995 Darmon–Diamond–Taylor exposition of the Wiles and Taylor–Wiles proof. After 11 days, at 02:00:57 UTC on August 18, the root of the graph was marked as proved.

In total, dev.to reports 29,500 intermediate theorems and about 6 billion output tokens, making the proof more than five times the size of Mathlib, Lean's standard mathematics library.

The mathematician's verdict

Buzzard's own effort carries a £1 million, five-year grant, and its plan alone runs to 86 pages. Anthropic lent him a machine with 500 GB of RAM; he compiled the more than 13.4 million lines himself and reported that the build took nearly 20 times as long as compiling Mathlib on a 96-core machine. His verdict was two-sided: the formalization checks out, and mathematically it "tells us essentially nothing". He was already 99.9 percent confident the theorem held, he wrote, and number theorists were fully confident; the formal proof follows the early literature and adds no new mathematics.

What excited him instead was the progress in autoformalization — converting human mathematics into machine-checkable form. The result also completes the last of Freek Wiedijk's formalization challenges, a list roughly 20 years old. On cost, Anthropic disclosed token counts but not dollars; commenters including David Jao estimated the roughly 6 billion output tokens at about $300,000 at prevailing API prices, excluding model training. Buzzard noted wryly that he was funded for five years while Anthropic finished in 11 days, but suspected they may have spent more money. He first heard about it by email while at the Green Man festival in Wales on poor connectivity, and initially dismissed the unknown sender as a crank.

Why it matters

The story is less about number theory than about how machine-generated artifacts earn trust. Thirteen million lines were accepted because they rest on a one-line statement, three standard axioms and two independently implemented kernels — the same shape as a small, carefully reviewed specification with a checker enforcing the implementation against it.

It also isolates the hard problem in multi-agent systems: the agents failed until they shared an explicit graph of what was proved and what remained open. Where the checker is strict, machine-written code that no human reads can still be sound; where it is not, the same volume of generated code is a liability.