← All repos

FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

GitHubimperialcollegelondon.github.io/FLT/
Browse cluster: Lean4 Formal Verification & Cryptography →
1,675commits
75contributors
7languages

Tech stack & purpose

FLT is an ongoing formalization of Fermat's Last Theorem in the Lean theorem prover, led by Kevin Buzzard at Imperial College London and funded by EPSRC until September 2029. The project formalizes a modern variant of the Wiles/Taylor-Wiles proof using ideas from Khare and Wintenberger, reducing the theorem to various mathematical results known by the 1980s, with formal statements of key assumptions documented in the repository. The codebase is written in Lean 4 and uses the Lake build system, with a Verso Blueprint package for authoring and rendering mathematical documentation alongside the formalization.

Community & reference links

Languages

Lean
86.5%
TeX
10.7%
Python
2.4%
Shell
0.2%
HTML
0.1%
CSS
0.1%
Perl
0.0%

Contributors (top 30 of 75)