Digitising the Langlands Program

朗兰兹哲学是一种深刻的思想集合，它将分析(对连续的研究)与算术(对离散的研究)联系起来。它可以追溯到20世纪60年代，但随着它的适用范围扩大到物理(几何朗兰兹计划)和非阿基米德情况(p-adic朗兰兹计划)，它的适用范围仍在扩大。朗兰兹哲学中引入的一些想法是精确的、定义明确的数学猜想，当然，多年来，一些猜想被证明了，现在成了定理。其他想法是更不稳定的概念，这些概念曾指导数学家，但从未完全精确。这在现代数学中并不少见！另一个也可以追溯到60年代的话题是形式证明助手理论--一种可以检查证明或检查数学陈述是否有意义的计算机程序。然而，与朗兰兹哲学形成鲜明对比的是，证明助手在数学系基本上是闻所未闻的，也许是因为直到最近，他们似乎只能理解群、平面图、球面等基本的本科生水平的对象。事实上，关于群、平面图和球面的一些极其深刻的问题已经使用证明助手进行了验证，非常遗憾的是，数学家并没有将这些工具视为潜在的机会。与以前的情况形成鲜明对比的是，我们将尝试使用证明助手来处理深刻而复杂的数学对象。特别是，我们将考虑自同构表示和伽罗瓦表示，以及朗兰兹哲学中思想的精确形式，这些形式最终被证明是精确的猜想。我们认为，有时我们这样做的尝试会失败，要么是因为文献中没有但专家知道的细节，要么是因为实际上没有人真正正确理解的细节。试图将这一哲学形式化将为它画上句号。并不是所有的数学家都有兴趣看到这条线--这条线是完整和严格的思想停止的地方，而更多变的一般原理是开始的地方。这绝对是数学家使用的情况，也需要严谨的思想和流畅的一般原理。然而，数学家通常对证明定理感兴趣，技巧是获得事物应该如何工作的概述，然后证明它们确实是以这种方式工作的。我们的方法是不同的。取而代之的是，我们将努力弄清楚*事情意味着什么*。希望这种对该地区的非标准调查将带来研究人员感兴趣的新问题。这项拨款的结果将是一个数学数据库，其中包含明确和准确的陈述，在计算机上形式化，人类和计算机都可以搜索。它还将是一份不稳定的原则清单，我们不能完全严格地理解其中的基本思想，因此，我们的社会面临着一项挑战，即分析这些原则，看看我们能否将它们转变为确切的现象，然后由该领域的专家进行研究。

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.