A machine-checked proof still needs a statement contract
Permanent archive: Zenodo · 10.5281/zenodo.22728950.
Anthropic's Fermat formalization shows the scale now possible in Lean; the remaining assurance problem is preserving meaning, provenance and dependency scope from source theorem to checked root.
What the laboratory reports
- Anthropic reports the first complete computer-checked proof of Fermat's Last Theorem, produced largely autonomously by Claude in Lean over 11 days.
- The final proof uses 29,500 intermediate theorems; Anthropic reports 13 million generated lines and a collaboration of dozens of agents.
- Early attempts lost track of project state. The successful workflow used Prove2Me to maintain a theorem dependency DAG, support search and reuse, and coordinate parallel work.
- Anthropic reports that Lean checked the finished proof, a comparator matched its root statement to Mathlib's FLT statement, and Kevin Buzzard reviewed the artifact.
The mathematical problem
Kernel acceptance establishes that a formal term has the encoded type under a particular axiom, library and toolchain environment. End-to-end assurance additionally requires a semantic commuting diagram: the intended natural-language theorem, the chosen formal root, imported definitions and the claimed conclusion must denote the same proposition. At this scale, provenance and change impact across the dependency DAG become part of correctness.
GERO's proposed response
- Package the formalization as a certificate-bearing claim graph with the root statement, axiom ledger, dependency DAG, library commits and toolchain hashes.
- Keep kernel verification, statement equivalence, source-to-formal mapping and provenance as separate verdicts rather than collapsing them into one 'proved' label.
- Prioritize independent review of high-centrality semantic bridges and require a clean replay from pinned artifacts before downstream reuse.
A falsifiable experiment
- Create controlled variants with one perturbation at a time: a changed root quantifier, a mismatched definition, an altered import and a stale dependency hash.
- Compare Lean compilation alone with the proposed statement-and-provenance contract on defect detection, false acceptance and expert review time.
- Repeat the clean build in an isolated pinned environment and record which assurance layers survive without access to the original agent workspace.
Read the primary source
This article is an original analytical summary, not a republication. Read Formalizing Fermat's Last Theorem for the laboratory's complete claims, methods and context.