Claude agents produce first computer-checked Lean proof of Fermat's Last Theorem

What happened

On September 4, Anthropic published the first complete, computer-checked proof of Fermat's Last Theorem, produced by a fleet of Claude agents working largely autonomously over 11 days, according to a dev.to write-up of the announcement. The proof is written in Lean, a proof assistant whose kernel verifies every logical step, and it covers a claim that went unproven for roughly 350 years.

Fermat jotted down his conjecture around 1637: no positive integers a, b and c satisfy aⁿ + bⁿ = cⁿ for any exponent greater than 2. Andrew Wiles proved it in 1995 with a 129-page argument, after a reviewer's question exposed a gap in his 1993 presentation that took a year to repair, first alone and then with his former student Richard Taylor. Rewriting that proof so a machine can check each step has been a community project since 2024, led by Kevin Buzzard at Imperial College London. Per the dev.to article, the blueprint for just the initial phase spans 86 pages, and the effort was scoped as a multi-year undertaking.

Tianyi Peng, an Anthropic researcher whose academic group at Columbia University builds AI formalization tools, set out to test whether Claude could make progress on it. The outcome, per Anthropic's own account, went well beyond incremental gains.

The scale of the run

As reported, the effort produced 13 million lines of Lean, more than five times the size of Mathlib, the community proof library it builds on, though Anthropic notes the proof is longer than it strictly needs to be. The agents proved 30,300 theorems, of which 29,500 feed the final artifact, and generated roughly six billion output tokens using an internal research model. Dozens of agents defined concepts, proved intermediate results and chained them together.

The failure that came first

The detail the dev.to author singles out is that the first attempts collapsed. Anthropic's post states that agents had some early success but then lost track of the project's state and stopped collaborating effectively. The model itself did not change between the failed runs and the successful one; the coordination layer did. Project state had lived inside the agents' context windows, which degrade over time, so one agent's picture of what was already proven diverged from another's.

The fix was Prove2Me, an open platform built by Peng and his Columbia collaborators. It maintained a directed acyclic graph of theorem statements that agents consulted to decide what to prove next, kept theorem statements and their proofs in separate files to speed up Lean compilation and cut resource use, and stored a natural-language description of every node so later agents could search for and reuse existing results instead of re-deriving them. The failed runs were not wasted: Anthropic says they contributed about 7 percent of the non-boilerplate lines in the final proof.

The dev.to piece frames this as giving agents a build system for theorems, comparable to how Make, Bazel and CI pipelines have scheduled work for decades, with each node acting as a deliverable that has an unambiguous completion criterion.

Human input shrank to prioritization. Peng's recorded nudges include "Jacobian as a scheme sounds high priority." The agents' own logs mark the finish line: "The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18."

How it was verified

Nobody read 13 million lines by hand. Lean's kernel checked every step, the proof relies only on Lean's three standard axioms with no omitted steps, and a comparator tool confirmed that the final theorem statement matches Mathlib's own statement of the theorem. Buzzard reviewed the result and, according to the dev.to article, wrote that if automatic formalization of FLT is possible now, a significant step has been taken toward automation in mathematics.

Why it matters

This is a landmark for autonomous AI research: a project scoped as a multi-year community effort was compressed into 11 days of largely unsupervised work, on a theorem famous precisely because it resisted the world's best mathematicians for centuries.

The more transferable lesson concerns the failure. The agents appear to have been capable of the work from the start; what they lacked was shared memory. Once project state moved out of context windows and into a dependency graph every agent could read and trust, the same models succeeded. Anyone running multiple agents against a shared codebase or pipeline will recognize the pattern, and the takeaway is that externalized state is a design decision, not a model capability.

It also underscores the role of mechanical verification. Autonomy at this scale was only tenable because Lean's kernel and a statement comparator could check the output; the trust sits in the gates rather than in the agents. Meanwhile the human contribution shifted from writing proofs to choosing what matters next.

One caveat: the figures and quotes here come from Anthropic's own post as relayed through a single secondary write-up, and that write-up cuts off before Buzzard's full commentary, so independent evaluation of the result is still pending.