{"id":"lean/anthropics__fermats-last-theorem","url":"https://github.com/anthropics/fermats-last-theorem/tree/main","repo":"https://github.com/anthropics/fermats-last-theorem","tags":["fermats-last-theorem","lean4","formal-verification","modular-forms"],"score":1,"title":"Fermat's Last Theorem in Lean 4","origin":"ai-generated","source":"lean","authors":["Anthropic"],"reviews":0,"subject":"math.NT","summary":"A complete, machine-checked Lean 4 proof of Fermat's Last Theorem, built on Mathlib: for every natural number n >= 3 there are no positive natural numbers a, b, c with a^n + b^n = c^n (declaration fermat_last_theorem). The default build target also derives Mathlib's own statement FermatLastTheorem. The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles; the named classical inputs (irreducibility of the Frey representation, Langlands-Tunnell, modularity lifting, modularity of semistable curves, level lowering) are proved within the development, in the strength the argument needs,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":3,"published":"2026-09-04","reactions":{"up":1,"🎉":1},"discussion":[{"url":"https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/","date":"2026-09-04","kind":"web","site":"Xena","text":"I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour later it was officially announced by Anthropic: one of their internal models, using the prove2.m…","added":"2026-11-04","title":"FLT: Anthropic has beaten me to it","author":"Kevin Buzzard"},{"url":"https://x.com/jdlichtman/status/2095959872563269840","date":"2026-09-04","kind":"x","added":"2026-11-04","author":"Jared Duker Lichtman","handle":"jdlichtman"},{"url":"https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/#:~:text=When%20Anthropic%20announced%20that%20Claude%20had%20formally%20verified%20Fermat","date":"2026-10-16","kind":"web","site":"Xena","text":"When Anthropic announced that Claude had formally verified Fermat’s Last Theorem with 13 million lines of code written over 11 days, Kevin Buzzard cheerfully lauded the result while also declaring he had no intention of ending his ongoing formalization of a more modern proof. Once again, although…","added":"2026-11-04","title":"How to Formalize All of Mathematics","author":"Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne et al."}],"formalized":true,"formalizes":[{"title":"Modular elliptic curves and Fermat's Last Theorem","identifier":"doi:10.2307/2118559","relationship":"formalizes"},{"title":"Ring-theoretic properties of certain Hecke algebras","identifier":"doi:10.2307/2118560","relationship":"formalizes"},{"title":"Fermat's Last Theorem","identifier":"In: Current Developments in Mathematics, 1995 (International Press), 1-154","relationship":"formalizes"}]}