Claude Autonomously Formalizes Fermat's Last Theorem in Lean
Source: Anthropic
Anthropic demonstrated that Claude translated a centuries-old mathematical proof into machine-verifiable code with minimal human intervention. The task required navigating multiple technical frameworks and iterating without reset—a shift from prompt-response cycles toward sustained, goal-directed work on problems demanding both deep understanding and precise execution. Formal verification is where mathematical rigor meets automation. If AI can handle this reliably without constant supervision, applications in theorem proving, code verification, and scientific formalization become concrete—work that previously required expert mathematicians full-time. The 11-day autonomous window matters less than what it required: Claude operating at project scale rather than single-turn reasoning.