权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Digitising the Langlands Program

朗兰兹计划数字化

基本信息

批准号：
EP/V048724/1
负责人：
Kevin Buzzard
金额：
$ 25.72万
依托单位：
Imperial College London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2021
资助国家：
英国
起止时间：
2021 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FV048724%2F1
关键词：
Digitising 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.

朗兰兹哲学是一个深刻的思想集合，它将分析（对连续的研究）与算术（对离散的研究）联系起来。它可以追溯到20世纪60年代，但随着其适用范围的扩大，它的适用范围还在不断扩大，包括物理学（几何朗兰兹纲领）和非阿基米德情况（p-adic朗兰兹纲领）。朗兰兹哲学中提出的一些思想是精确的、定义明确的数学命题，当然，这些年来，有些命题被证明了，现在是定理。其他的思想是一些更不固定的概念，它们指导着数学家，但从未被完全精确化。这在现代数学中并不罕见！另一个可以追溯到60年代的主题是形式证明助手的理论--可以检查证明或检查数学陈述是否有意义的计算机程序。然而，与朗兰兹哲学形成鲜明对比的是，证明助手在数学系中基本上是闻所未闻的，也许是因为直到最近，他们似乎只能理解基本的本科水平的对象，如群，平面图，球体等。事实上，一些关于群，平面图和球体的极其深刻的问题已经使用证明助手进行了验证，很遗憾，数学家们并没有将这些工具视为一个潜在的机会。与以往形成鲜明对比的是，我们将尝试使用证明助手来处理深刻而复杂的数学对象。特别地，我们将考虑自守表示和伽罗瓦表示，以及朗兰兹哲学中的观念的精确形式，这些形式最终被证明是精确的表述。我们相信，有时候我们这样做的尝试会失败，要么是因为文献中没有但专家知道的细节，要么是因为没有人真正正确理解的细节。试图将哲学形式化将在其中画一条线。不是所有的数学家都有兴趣看到这条线--这是完整和严格的思想停止的地方，更易变化的一般原则开始。数学家使用和需要严格的思想和流动的一般原理，这绝对是事实。然而，数学家通常对证明定理感兴趣，而技巧是获得事物应该如何工作的概述，然后证明它们确实以这种方式工作。我们的方法不同。我们将试图弄清楚 * 事物的含义 *。希望这种对该领域的非标准调查能提出研究人员感兴趣的新问题。这笔赠款的成果将是一个数学数据库，其中包含明确而精确的陈述，在计算机上正式化，并可供人类和计算机搜索。此外，这份报告亦会列出一些不稳定的原则，我们无法完全准确地理解其背后的理念，因此，我们的社会亦须对这些原则作出分析，看看能否把它们转化为精确的现象，然后由这方面的专家加以研究。