Formalizing Fermat's Last Theorem

Subscribe to Anthropic Science Features on AI-assisted discoveries, practical workflows, and field notes across the sciences. We are sharing the first complete computer-checked proof of Fermat’s Last Theorem. Claude worked largely autonomously over 11 days to write the proof in the Lean programming language. Below, we describe how the formalization was done and share some thoughts about what this ...