Measured acceleration · Mathematics · Computer science
Claude completes an independently checked Lean formalization of Fermat’s Last Theorem
A complete Lean proof of Fermat’s Last Theorem with standard axioms and a statement checked against Mathlib.
Summary
Anthropic released a complete formalization produced largely autonomously over 11 days. Kevin Buzzard independently compiled the repository and ran comparator, confirming that it checks. The release supplies verification scripts and an inspectable dependency structure.
AI role
Claude agents used Prove2Me to organize dependencies, generate intermediate proofs, and assemble a formalization of the established Wiles–Taylor–Wiles argument.
Narrative role
This demonstrates automation at the scale of a major mathematical verification project and supplies external checking beyond the developer’s announcement.
Caveat
This formalizes known mathematics, drawing on human proofs and community libraries. The reported development time excludes those foundations; the large research artifact is not a maintained Mathlib contribution.