AI Agents Machine-Check a Full Proof of Fermat's Last Theorem in Lean 4

Anthropic has released a complete, machine-verified formalization of Fermat’s Last Theorem in the Lean 4 proof assistant, built on the Mathlib library. The proof follows the classical Frey–Serre–Ribet–Wiles–Taylor-Wiles route and was produced by AI agents working on top of human-written open-source Lean — most notably Kevin Buzzard’s Imperial College FLT project, the flt-regular library, and Mathlib itself. The final theorem states, in Lean’s built-in naturals, that a^n + b^n ≠ c^n for positive a, b, c and n ≥ 3, and the repository spans 60,475 modules and roughly 29,500 theorems.

What makes the artifact notable is the verification discipline layered around it. The build fails unless the proof rests on exactly Lean’s three standard axioms, with no sorry, no injected axioms, and no native_decide or other trust-widening escape hatches. Beyond the Lean kernel itself, the team ran leanprover’s comparator to confirm the proved statement is identical to a Mathlib-only challenge statement, then replayed the entire environment through nanoda, an independent Lean kernel written in Rust, which accepted all 1,052,234 declarations. The checks are expensive — the comparator kernel replay alone took nearly 15 hours on one core, and the full build peaked above 150 GB of memory.

The practical significance is less about the mathematics, which has been settled since Wiles, than about the method: autonomous agents assembling and closing a proof at this scale, with correctness delegated entirely to a mechanical kernel that leaves no room for hand-waving. The sources are explicitly written to be checked rather than read — names are machine-generated and comments stripped — making the Lean statement, not human legibility, the source of truth. It ships as an unmaintained research artifact under Apache 2.0, including a 390 MB offline HTML browser for the proof, and stands as a concrete demonstration of AI-driven formal reasoning verified end to end.