Anthropic's Claude formally proves Fermat's Last Theorem
Anthropic just open-sourced the first complete, machine-checked proof of Fermat's Last Theorem in Lean 4, generated entirely by AI agents. Spanning over 13 million lines of code and 29,511 theorems, the massive artifact successfully passed checks by two independent verification kernels without extra axioms. It marks a historic milestone for AI-driven mathematics.