fermats-last-theorem

This repository presents a complete, machine-checked proof of Fermat's Last Theorem in Lean 4, built on Mathlib, following the argument of Frey, Serre, Ribet, Wiles and Taylor-Wiles. The main theorem, fermat_last_theorem, states that for n ≥ 3 and positive natural numbers a, b, c, a^n + b^n ≠ c^n. The default build fails unless the proof rests only on Lean's three standard axioms. The build was checked with the comparator tool, and an independent kernel, nanoda 0.4.13, accepted the same environment, which the article reports contains 1052234 declarations. The repository is a research artifact that is not maintained or accepting contributions.