{"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":0,"published":"2026-09-04","reactions":{"up":1,"🎉":1},"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"}]}