# Digitising the Langlands Program

Lead Research Organisation: Imperial College London
Department Name: Mathematics

### Abstract

The Langlands Philosophy is a profound collections of ideas which relates analysis (the study of the continuous) to arithmetic (the study of the discrete). It dates back to the 1960s but is still growing as its domain of applicability expands to cover things such as physics (the geometric Langlands program) and non-archimedean situations (the p-adic Langlands program).

Some of the ideas introduced in the Langlands Philosophy are precise well-defined mathematical conjectures, and of course over the years some of the conjectures were proved and are now theorems. Other ideas are more fluid concepts which have guided mathematicians without ever being made completely precise. This is not at all uncommon in modern mathematics!

Another topic which also dates back to the 60s is the theory of formal proof assistants -- computer programs which can check proofs or check that mathematical statements make sense. However, in stark contrast to the Langlands philosophy, proof assistants are essentially unheard of in mathematics departments, perhaps because until recently they seemed to be only able to understand basic undergraduate level objects such as groups, planar graphs, spheres and so on. In fact some extremely profound questions about groups, planar graphs and spheres have been verified using proof assistants, and it is a great pity that mathematicians do not view these tools as a potential opportunity.

In stark contrast to what has gone before, we will attempt to engage with profound and complex mathematical objects using a proof assistant. In particular we will consider automorphic representations and Galois representations, and *state* precise forms of the ideas in the Langlands philosophy which turn out to be precise conjectures. We believe that sometimes our attempts to do this will fail, either because of details which are not in the literature but which experts know, or because of details which nobody actually understands properly.

Attempting to formalise the philosophy will draw a line through it. Not all mathematicians are interested in seeing this line -- it is the line where the complete and rigorous ideas stop, and the more fluid general principles start. It is absolutely the case that mathematicians use and need both rigorous ideas and fluid general principles. However mathematicians are usually interested in proving theorems, and the technique is to get an overview of how things should work, and then prove that they do work in this way. Our approach is different. We will instead try to figure out *what things mean*. The hope is that this kind of non-standard investigation of the area will raise new questions of interest to researchers.

The outcome of this grant will be a mathematical database of unambiguous and precise statements, formalised on a computer, and searchable by both humans and computers. It will also be a list of fluid principles for which we cannot make completely rigorous sense of the underlying ideas, and hence a challenge to our community to analyse these principles to see if we can turn them into precise phenomena which can then be worked on by experts in the area.

### ORCID iD

Kevin Buzzard (Principal Investigator)  http://orcid.org/0000-0002-7187-5109

### Publications

10 25 50
Buzzard K (2021) Schemes in Lean in Experimental Mathematics

Frutos-Fernández M.I.D. (2022) Formalizing the Ring of Adèles of a Global Field in Leibniz International Proceedings in Informatics, LIPIcs

Maria Ines De Frutos-Fernandez, (2022) Formalizing the Ring of Adeles of a Global Field

Description Within the first year of the grant, my post-doc Maria Ines de Frutos Fernandez showed that it was possible to teach to a computer the statements of the main theorems of global class field theory. In the second year, she began the long and complex task of teaching a computer the proofs of the main theorems of local class field theory. Since her time here she has been offered two more post-docs and I'm sure will soon be being offered tenure positions. The grant has launched her career; she is about to have a piece on her subject area, featuring her, appearing in popular science magazine Quanta.
Exploitation Route Maria Ines and I are part of a team making a gigantic formalised mathematical library, whose aim is to cover a standard Masters degree and then move on towards current research. The library is already been used by companies such as OpenAI, Facebook, DeepMind and others who are attempting to make systems which can automatically generate formally verified answers to mathematical questions.
Sectors Digital/Communication/Information Technologies (including Software)

Education

Description Tech companies are using the libraries which we are developing in order to create systems which are beginning to have some kind of understanding of modern mathematics.
First Year Of Impact 2021
Sector Digital/Communication/Information Technologies (including Software),Education