Formalising Fermat

数学可以被视为有精确规则的游戏--一切都是黑白分明的。如今，计算机在这类游戏中变得非常擅长。计算机通常可以在国际象棋中击败最好的人类，随着Deep Mind最近的新开发，它们现在可以在东方棋盘游戏围棋中击败我们。事实上，计算机科学家现在认为棋类游戏基本上已经被“解决”了--计算机比人类玩得更好。但数学是不同的--它天生就是无限的。由于这样或那样的原因，在证明新的数学定理的游戏中，计算机目前还远远不能“击败”人类。然而，目前在研究范围内的是，计算机可以用来“帮助”数学家进行研究，做的事情从自动检查杂乱无章的引理到建议在特定情况下可能有用的结果。也许令人惊讶的是，这种进步的主要障碍是，从事这类软件的数学家太少，因此计算机验证助理根本不知道数学家在研究中使用的对象的大多数*定义*，更不用说关于这些定义的主要定理了。计算机科学家已经设计了工具，可以分析定理的数据库，并自动提出建议或应用它们--问题是数据库还不存在。拟议的研究旨在改变这一点。Wiles和Taylor-Wiles在1994年解决了费马大定理，这是20世纪数学的一大亮点，所使用的工具(自同构形，伽罗瓦表示)至今仍是数论的中心研究对象。我的建议是在精益计算机证明助手中完全形式化现代证明中涉及的许多数学，从而将完全形式化费马大定理的证明的(巨大)任务减少到完全形式化20世纪80年代的各种结果的任务。这样的项目将使Lean能够理解现代数论和算术几何中的许多基本定义，这意味着可以开始陈述使用这种机器的数论和算术几何中的现代数学猜想和定理。最终，该项目的结果将是计算机将能够理解20世纪末数学的一些证明，以及21世纪数学的许多定理陈述。特别是，这个项目使人类能够开始考虑创建现代数论结果的正式数据库。人们可以设想一种计算机形式的服务版本，比如为人类总结现代数学研究论文的数学评论，或者可以由人工智能研究人员挖掘的代数和算术几何结果数据库。

Mathematics can be viewed as a game with precise rules -- everything is black and white. Computers are nowadays getting very good at such games. Computers can routinely beat the best humans at chess, and with the recent new developments by Deep Mind they can now beat us at the oriental board game Go. Indeed, computer scientists now consider board games to be essentially "solved" -- computers play them better than humans. But mathematics is different -- it is inherently infinite. For this and other reasons, computers are currently nowhere near "beating" humans at the game of proving new mathematical theorems. However, what is currently within scope is that computers could be used to *help* mathematicians with their research, doing things from checking messy lemmas automatically to suggesting results which may be helpful in a given situation. Perhaps surprisingly, the main obstacle to this sort of progress is that too few mathematicians are engaged with this kind of software, and hence computer proof assistants simply do not know most of the *definitions* of the objects which mathematicians use in their research, let alone the main theorems about these definitions. Computer scientists have already designed tools which can analyse databases of theorems and make suggestions or apply them automatically -- the problem is that the databases do not yet exist.The proposed research intends to change this. The resolution by Wiles and Taylor-Wiles of Fermat's Last Theorem in 1994 was a highlight of 20th century mathematics, and the tools used (automorphic forms, Galois representations) are still central objects of study in number theory today. My proposal is to fully formalise much of the mathematics involved in a modern proof of FLT in the Lean computer proof assistant, thus reducing the (gigantic) task of fully formalising a proof of Fermat's Last Theorem to the task of fully formalising various results from the 1980s. Such a project will enable Lean to understand many of the basic definitions in modern number theory and arithmetic geometry, meaning that it will be possible to start stating modern mathematical conjectures and theorems in number theory and arithmetic geometry which use such machinery.Ultimately the outcomes of the project will be that a computer will be able to understand some proofs from late 20th century mathematics, but also many statements of theorems of 21st century mathematics. In particular, this project enables humanity to start thinking about creating formalised databases of modern results in number theory. One could envisage a computer-formalised version of the services such as Math Reviews which summarise modern mathematical research papers for humans, or databases of results in algebraic and arithmetic geometry which can be mined by AI researchers.