EPSRC logo

Details of Grant 

EPSRC Reference: EP/Y022904/1
Title: Formalising Fermat
Principal Investigator: Buzzard, Professor K
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Mathematics
Organisation: Imperial College London
Scheme: EPSRC Fellowship
Starts: 01 October 2024 Ends: 30 September 2029 Value (£): 934,043
EPSRC Research Topic Classifications:
Algebra & Geometry
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
11 Sep 2023 EPSRC Mathematical Sciences Fellowship Interview Panel 12 and 13 September 2023 Announced
18 Jul 2023 EPSRC Mathematical Sciences Prioritisation Panel July 2023 Announced
Summary on Grant Application Form
Mathematics can be viewed as a game with precise rules -- everything is black and white. Computers are nowadays getting very good at such games. Computers can routinely beat the best humans at chess, and with the recent new developments by Deep Mind they can now beat us at the oriental board game Go. Indeed, computer scientists now consider board games to be essentially "solved" -- computers play them better than humans.

But mathematics is different -- it is inherently infinite. For this and other reasons, computers are currently nowhere near "beating" humans at the game of proving new mathematical theorems. However, what is currently within scope is that computers could be used to *help* mathematicians with their research, doing things from checking messy lemmas automatically to suggesting results which may be helpful in a given situation. Perhaps surprisingly, the main obstacle to this sort of progress is that too few mathematicians are engaged with this kind of software, and hence computer proof assistants simply do not know most of the *definitions* of the objects which mathematicians use in their research, let alone the main theorems about these definitions. Computer scientists have already designed tools which can analyse databases of theorems and make suggestions or apply them automatically -- the problem is that the databases do not yet exist.

The proposed research intends to change this. The resolution by Wiles and Taylor-Wiles of Fermat's Last Theorem in 1994 was a highlight of 20th century mathematics, and the tools used (automorphic forms, Galois representations) are still central objects of study in number theory today. My proposal is to fully formalise much of the mathematics involved in a modern proof of FLT in the Lean computer proof assistant, thus reducing the (gigantic) task of fully formalising a proof of Fermat's Last Theorem to the task of fully formalising various results from the 1980s. Such a project will enable Lean to understand many of the basic definitions in modern number theory and arithmetic geometry, meaning that it will be possible to start stating modern mathematical conjectures and theorems in number theory and arithmetic geometry which use such machinery.

Ultimately the outcomes of the project will be that a computer will be able to understand some proofs from late 20th century mathematics, but also many statements of theorems of 21st century mathematics. In particular, this project enables humanity to start thinking about creating formalised databases of modern results in number theory. One could envisage a computer-formalised version of the services such as Math Reviews which summarise modern mathematical research papers for humans, or databases of results in algebraic and arithmetic geometry which can be mined by AI researchers.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.imperial.ac.uk