Anthropic uploads machine-verified Lean 4 proof of Fermat's Last Theorem

Chris_Armstrong · x · 2026-09-05

Per accounts circulating on X, Anthropic has uploaded a Lean 4 formalization of Fermat's Last Theorem — translating one of mathematics' most legendary theorems into a fully machine-checkable proof. Details are described in Anthropic's official write-up.

Related event: Claude completes first formal proof of Fermat's Last Theorem in Lean(23 posts)→

Original post →

More from Research

Research channel →