Formalising Fermat

形式化费马

• 批准号: EP/Y022904/1
• 负责人: Kevin Buzzard
• 金额: $ 119.02万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2024
• 资助国家: 英国
• 起止时间: 2024 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY022904%2F1
• 关键词: Formalising; Fermat

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.

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