Editorial note
A single repository is the lead story today: a massive, machine‑checked formalization of Fermat’s Last Theorem built with AI agents and verified by independent kernels. Beyond the headline, the artifact exposes practical questions about provenance, trust, and how mathematicians and engineers will treat AI‑assembled proofs.
In Brief
Fermat's Last Theorem in Lean 4
Why this matters now: Anthropic’s Fermat’s Last Theorem repo claims a complete, machine‑checked version of a century‑old headline theorem, showing AI agents can assemble very large formal proofs that are kernel‑verifiable.
Anthropic published a repository that presents "a complete, machine-checked proof of Fermat's Last Theorem in Lean 4" built on Mathlib, reportedly spanning roughly 13 million lines of Lean code and 60k+ modules. The authors provide an offline HTML reader so anyone can open index.html and browse the artifact without a server; they also note the sources were checked by the Lean 4 kernel and an independent Rust kernel (nanoda). The project is framed as a research artifact — heavy to reproduce, not intended as an actively maintained library, and reportedly produced with AI agents building on existing human‑written Lean work.
"Open html/index.html in a web browser; everything works offline, with no web server."
Deep Dive
Fermat's Last Theorem in Lean 4
Why this matters now: A machine‑checked Fermat, if accurate, changes how mathematicians and verification engineers think about large‑scale formalization: AI can assemble enormous, kernel‑verifiable proofs, forcing a rethink about provenance, review, and compute costs.
The scale here is important and unusual. Anthropic's artifact isn't a compact human‑written manuscript: it's an enormous formal library meant to reproduce the Frey–Serre–Ribet–Wiles chain within the Lean ecosystem. That size matters because formal verification is only as useful as its dependencies and the trust you place in them. The repository's authors try to address that by saying the "final statement depends only on three standard axioms" and by rechecking the result with two independent kernels — a meaningful step toward minimizing single‑implementation errors.
Equally notable is the claimed role of AI agents in producing the Lean sources. This isn't a small helper script; Anthropic says agents built on human‑written mathlib produced the bulk of the files. That highlights a new workflow: AI assembles formal components, humans or kernels validate them, and the artifact stands or falls on kernel checks and human interpretability. The kernel verifies syntactic and logical correctness, but it can't tell you whether a lemma's name or the project's structure matches human mathematical intent — humans still need to audit whether "what the proof says" is the proof "you meant."
Practical barriers are real. Building and verifying the full artifact is computationally heavy — the project requires hundreds of gigabytes of RAM and many hours on large machines — so independent reproduction is nontrivial. That raises two immediate points: first, reproducibility for the broader community will be limited to those with substantial compute; second, verification budgets and tooling will become an infrastructure concern for formal math, just like large compute is for ML research.
What should practitioners and mathematicians watch next? A few concrete signals:
- Whether external experts publish independent audits that trace the machine‑checked steps back to recognizable human arguments.
- Tooling improvements that make large formal artifacts exploreable without huge memory footprints (the provided offline HTML is a good start).
- Discussion around credit and authorship when AI agents assemble proofs: who gets cited, and how are human contributions recorded?
Bold takeaway: Kernel verification is necessary but not sufficient — a kernel says the formal chain is consistent; it doesn't replace careful human readthrough to confirm that lemmas, motivations, and definitions match the intended mathematics.
Community reactions have mixed awe and levity: some readers treated this as a milestone for formalization tooling; others couldn't resist jokes about Fermat's marginal note. Regardless of tone, the practical conversation centers on provenance — how the sources were produced — and on whether similarly sized artifacts are now feasible for other big theorems.
A modest checklist for teams thinking about similar work:
- Prioritize independent kernel checks and reproducible build instructions.
- Archive provenance metadata: which models, prompts, and human edits produced each file.
- Budget for verification compute; plan for partial checks for reviewers with smaller resources.
Closing Thought
A machine‑checked Fermat isn't just a math stunt — it's a stress test for verification culture. The kernels can vouch for logical soundness, but the community will need readable provenance, independent audits, and practical tooling to treat AI‑assembled formal proofs as first‑class mathematical artifacts.