Fermat's Last Theorem 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. Until September 2029 it is being 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 info...