Digitising the Langlands Program

点击翻译按钮获取中文摘要

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.