Anthropic Open-Sources Agent-Generated Lean 4 Proof of Fermat's Last Theorem
Anthropic open-sourced a complete, machine-checked proof of Fermat's Last Theorem in Lean 4. Built by AI agents on top of Mathlib, the repository verifies across 29,511 theorems using independent Lean and Rust kernels without custom axioms.
Impact: Medium
Why it matters
Inspect an end-to-end agentic formal verification pipeline and reproduce independent kernel checks locally.
TL;DR
- 01AI agents synthesized a full formal proof spanning 29,511 theorems without compromising core axioms.
- 02Verified independently by both the Lean kernel and nanoda (Rust) with zero unproven sorry gaps.
- 03Demands heavy compute to replay: up to 300 GB RAM and 15 hours of single-core comparator execution.
Key facts
- Theorems checked
- 29,511
- Total declarations verified
- 1,052,234
- Lean toolchain
- Lean 4.33.1 (Mathlib v4.33.0)
- Peak memory requirement
- 300 GB (comparator replay)
- Secondary verification kernel
- nanoda 0.4.13 (Rust)
Machine-Checked Proof Architecture
The repository contains 60,475 modules proving fermat_last_theorem in Lean 4.33.1 with Mathlib v4.33.0. The build target FinalCheck.lean enforces that the proof depends solely on Lean's three standard axioms: propext, Classical.choice, and Quot.sound. The codebase contains no sorry, axiom, native_decide, unsafe, extern, or partial def.
Multi-Kernel Independent Verification
Anthropic verified the proof through two distinct checkers. First, leanprover/comparator checked the proof against verification/comparator/Challenge.lean in approximately 14 hours and 46 minutes on a single core, peaking at 230 GB RAM. Second, the independent Rust-based Lean kernel nanoda (version 0.4.13) checked all 1,052,234 exported declarations in 30 minutes across 16 threads, using 40 GB RAM.
Pipeline and Reproduction Steps
The Lean sources were synthesized by AI agents using pipeline labels (such as P2M and hex suffixes) and are optimized for machine verification rather than human reading. Reproduction requires Linux or macOS, elan, and Mathlib compiled from source. Parallel builds consume ~5 GB RAM per job (up to 36 GB on specific modules) and 67 GB of disk space under .lake/. A static browser viewer in html/ provides offline dependency graphs for 29,511 theorems.
Try it in 2 minutes
git clone https://github.com/anthropics/fermats-last-theorem flt && cd flt
LEAN_NUM_THREADS=96 lake build
verification/comparator/run.sh
verification/nanoda/run.shbash
✓ When to use
- Use to study how agent swarms can generate formal proof scripts targeting formal proof assistants.
- Use as a benchmark suite for testing alternative Lean kernels, type-checkers, and Lake build pipelines.
✕ When NOT to use
- Do not use this repository as a production mathematical library; Anthropic explicitly marked it unmaintained.
- Do not run comparator or full Lake builds on machines with under 64 GB RAM without limiting parallel jobs.
What to do today
- Clone the repository and inspect the lakefile.lean setup for pinned Lean 4.33.1 toolchains.
- Open html/index.html locally to explore agent-generated theorem dependency structures offline.
- Review verification/comparator/Challenge.lean to see how formal math challenge criteria are constructed.
What the community says
“I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No 'good faith' Lean proofs have every been shown faulty”
“Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there... I wonder if AI could develop this skill too through a process of efficiently refactoring”
Sources