Skip to content

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

License

Notifications You must be signed in to change notification settings

ImperialCollegeLondon/FLT

Folders and files

NameName
Last commit message
Last commit date

Latest commit

2d142bb · Jan 23, 2025
Jan 6, 2025
May 8, 2024
Jan 23, 2025
Jan 21, 2025
Oct 28, 2024
Oct 25, 2024
Nov 30, 2024
Nov 4, 2024
Oct 16, 2024
Oct 31, 2024
Apr 30, 2024
Nov 19, 2023
Nov 7, 2024
Apr 4, 2024
Jan 23, 2025
Jan 18, 2025
Jan 18, 2025
Nov 25, 2023

Repository files navigation

Fermat's Last Theorem

Website Documentation Blueprint Paper Gitpod Ready-to-Code

An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover.

Information about the project

The project is currently being led by Kevin Buzzard. From October 2024 it will be funded by grant EP/Y022904/1, awarded by the EPSRC. The project is hosted at Imperial College London. Kevin would like to extend many many thanks to both of these institutions for their ongoing support of this nonstandard research.

General information ("What is Fermat's Last Theorem/Lean?" / "Why are you doing this?" etc) is here.

The route we will be taking was planned out essentially entirely by Richard Taylor in discussions with Buzzard. It is a modern variant of the original Wiles/Taylor-Wiles proof. For more details about the mathematics behind the proof, a good place to start is the blueprint.

Information on how to contribute is available here.