Anthropic says Claude worked "largely autonomously" over 11 days to formalize the proof of Fermat's Last Theorem in the Lean programming language (Anthropic)

Anthropic announced that its AI model, Claude, autonomously formalized the proof of Fermat's Last Theorem in the Lean programming language. This achievement involved Claude working largely independently over an 11-day period to produce the first complete computer-checked proof of the theorem. The company highlighted this as a significant milestone in AI's capability for complex mathematical formalization.