Claude Formalizes Fermat’s Last Theorem

This is less an AI theorem-discovery milestone than a watershed for autoformalization: the breakthrough is translating deep existing mathematics into a kernel-checkable artifact at unprecedented speed. Prove2Me’s theorem DAG, parallel agents, reusable statements, and compilation workflow mattered as much as Claude’s raw reasoning ability. Buzzard notes the formalization follows an established proof and adds no new mathematics; its value is verification, reuse, and scale. Lean and an independent Rust kernel checked the artifact under Lean’s three standard axioms, while the repository warns that humans must still judge whether theorem statements mean what their generated names suggest. The workflow is resource-intensive: Anthropic reports roughly six billion output tokens, while the full verification process requires substantial compute, memory, and disk. For developers, the clearest signal is that structured scaffolding can turn long-horizon AI coding into auditable scientific infrastructure.