Fermat's Last Theorem, end-to-end Lean formalization

Anthropic end-to-end formalization

Model / AI: Anthropic research model

Anthropic reports that AI agents produced a complete Lean 4 formalization in eleven days, with high-level steering by Tianyi Peng. The repository derives Mathlib's FermatLastTheorem, restricts dependencies to Lean's three standard axioms, and records successful checks by Lean, Comparator and the independent nanoda kernel. Kevin Buzzard independently ran Comparator and audited the non-mathematical surface for soundness issues.

Source read 2026-09-08. Read the repository's statement, attribution and verification sections, Anthropic's announcement, Nature coverage and Buzzard's independent account. The very large build was not rerun.

• Lean — Lean repository
• Context — Anthropic announcement
• Context — Independent audit by Kevin Buzzard
• News — Nature coverage