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 reports that its Claude model independently formalized the proof of Fermat’s Last Theorem in the Lean proof assistant over an 11-day period. The effort demonstrates Claude’s capability to autonomously handle complex mathematical formalization tasks without human intervention.