GoKawiilFully machine-checked Lean 4 proof of Fermat's Last Theorem released as research artifact
A complete formalization of Fermat's Last Theorem has been written and verified in the Lean 4 proof assistant, built atop the Mathlib library and following the Frey-Serre-Ribet-Wiles-Taylor-Wiles argument. The repository builds all 60,475 modules from scratch, with every declaration checked by the Lean kernel, and the final theorem relies solely on Lean's three standard axioms rather than any sorry or added axiom. An independent tool, leanprover/comparator, confirmed the proved statement matches a separately stated Mathlib-only challenge and that the entire proof chain replays correctly.