Fermat’s Last Theorem — no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for n > 2 — sat unproven for 350 years after Fermat claimed a “marvelous proof” his margin was too narrow to contain. Andrew Wiles proved it in 1995 with a 129-page argument, and even that nearly collapsed: a reviewer’s question exposed a gap that took Wiles a year to fix.

Anthropic says Claude has now produced the first proof a computer can check end to end. In 11 days, working largely autonomously, a team of collaborating Claude agents wrote roughly 13 million lines in Lean — a “proof assistant” language that verifies every logical step — proving about 30,000 intermediate theorems along the way. Translating a proof into this form is called formalization, and it is brutally tedious for humans: Lean needs to see every step, however trivial. A community effort had expected to take years.

The interesting part is how the agents pulled it off:

  • Earlier attempts failed — agents lost track of the project’s state and stopped collaborating effectively.
  • The breakthrough was Prove2Me, an open platform that keeps a graph of theorem statements so agents always know what to attempt next, mitigates their memory degradation, and lets dozens work in parallel.
  • Human input was limited to occasional high-level nudges like “Jacobian as a scheme sounds high priority.”
  • The finished proof was verified against Lean’s three standard axioms, and a comparator confirmed it states exactly the theorem mathematicians mean.

Why does this matter beyond one theorem? Human verification of math is slow and fallible — the Kepler conjecture spent four years in review and settled for “99% certain”; some wrong results stand for years. If AI can formalize proofs, it can check LLM-written mathematics and catch errors in the existing literature. Kevin Buzzard, the Imperial College mathematician leading the community formalization effort, called it “a big step towards automatic formalization of the modern mathematical literature.”

It also quietly demonstrates the pattern of humans supervising agent swarms: a small team, a coordination platform, and high-level direction — with the agents doing millions of lines of intermediate work.