Anthropic Uses Claude to Formalize Fermat's Last Theorem

Anthropic demonstrated that Claude can translate Andrew Wiles's 1995 proof of Fermat's Last Theorem into machine-verifiable code—a task requiring the AI to navigate both symbolic logic and mathematical intuition at scale. Large language models are becoming viable tools for mathematical formalization, a domain where AI has historically stumbled on rigor. The capability opens concrete applications for formal verification in cryptography, chip design, and financial systems, where a single logical flaw cascades into real costs.