Anthropic's Claude Spends 11 Days Formalizing Fermat's Last Theorem in Machine-Checked Code

Anthropic says a team of its Claude models has produced the first complete, machine-checked formalization of the proof of Fermat's Last Theorem, working largely autonomously over 11 days to turn Andrew Wiles's celebrated 1995 argument into code a computer can verify line by line. The project, detailed in a research report Anthropic published this week, tackles a claim Pierre de Fermat scribbled in a margin in 1637 and that took 358 years to settle: that no three positive integers a, b, and c can satisfy a^n + b^n = c^n for any whole number n greater than two.