Digitising the Langlands Program

朗兰兹哲学是将分析（对连续的研究）与算术（对离散的研究）联系起来的思想的深奥集合体。它可以追溯到20世纪60年代，但随着它的应用范围扩大到物理学（几何朗兰兹程序）和非阿基米德情况（p进朗兰兹程序）等领域，它仍在不断发展。《朗兰兹哲学》中引入的一些思想是精确定义的数学猜想，当然，多年来，其中一些猜想得到了证明，现在已经成为定理。其他思想则是一些不确定的概念，它们指导着数学家们，但却从未完全精确过。这在现代数学中并不罕见！另一个可以追溯到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.