Claude formalized Fermat's Last Theorem in Lean

Anthropic says Claude has formalized Fermat’s Last Theorem in Lean, the proof assistant used to write mathematics in a form that software can check. The company says the model worked largely autonomously for 11 days to turn the famous theorem into a verified formal proof.

The point is not that Claude discovered a new proof. Fermat’s Last Theorem was already proved by Andrew Wiles, and the hard mathematical result was known. What is new here is the translation of that proof into a machine-checkable formalization, a task that usually demands deep mathematical knowledge, patience, and fluency with proof-assistant tooling.

That matters because formal proof work is one of the places where AI progress can be measured with unusual clarity: either the proof checks, or it does not. If models can reliably assist with this kind of work, mathematicians and technical researchers may get faster ways to verify arguments, port results into formal libraries, and reduce the manual labor around proof engineering.

Anthropic frames the result as an early sign of how AI systems could support research mathematics, while leaving open the harder question of how broadly this ability transfers beyond one high-profile formalization.