Formalizing Fermat's Last Theorem in Lean: An Open Source Project

An ambitious open-source project aims to formally prove Fermat's Last Theorem using the Lean theorem prover. Led by Kevin Buzzard and funded by the EPSRC, hosted at Imperial College London, the project employs a modern variant of the original Wiles/Taylor-Wiles proof, planned in collaboration with Richard Taylor. The project website provides details on Fermat's Last Theorem, the Lean prover, project goals, and contribution guidelines.