走进科学
费马大定理的形式化项目
费马大定理形式化项目，旨在通过现代数学方法让计算机理解这一经典定理的证明。
引言
费马大定理(FLT)声称某个抽象方程在正整数中无解。这一结果没有实际应用。那么，为什么Andrew Wiles在1993年解决这个问题的消息登上了《纽约时报》的头版呢？
FLT的一个方面是，它的表述非常简单(若n≥3，则方程[x^n + y^n = z^n]在正整数中无解)，但证明极其困难(数学界花了350多年才完成)。这让人深刻地认识到数学的奥妙所在。然而，真正引发人们对这个问题兴趣的是，几个世纪以来，为了解决这个问题，大量数学理论被开发出来，其中很多理论从密码学到物理学都得到了应用。Wiles或许是受FLT的激励，但最终他的工作成为了Langlands计划中的一项突破，这个计划包含了许多尚未解决的猜想，并在2024年依然备受关注。而在历史上，代数数论中的几次重要突破(如数域中的分解理论和圆分域的算术研究)至少部分受到了揭示FLT的动机驱动。
Wiles的工作由Taylor-Wiles完成，建立在20世纪数学的巨大基础之上。此外，Wiles引入的基本技术(一个“模性提升定理”)在其原始论文发表后的30年里得到了概念上的简化和极大推广。直到今天，这个领域依然非常活跃。Frank Calegari在2022年的ICM论文中回顾了自Wiles突破以来的发展。这一领域的持续活跃是我启动FLT形式化证明项目的部分动机之一。
数学的形式化
数学的形式化是一门艺术，它将纸面上的数学翻译成足够丰富的计算机编程语言，以理解定理和证明的概念。这些编程语言，也称为交互式定理证明器(ITPs)，已经存在了几十年。然而，近年来，这一领域似乎引起了部分数学界的关注。我们已经看到了一些现代研究数学被实时形式化的例子，最新的一例是Tao等人在解决多项式Freiman-Ruzsa猜想的工作。这个2023年的突破性论文在短短三周内就被用Lean形式化了。像这样的成功案例可能会让外行人相信像Lean这样的ITP已经准备好形式化所有现代数学。然而，事实远非如此。在某些数学领域，比如组合数学，我们确实看到一些现代突破可以实时形式化。然而，我定期参加伦敦数论研讨会，每周我都注意到Lean甚至无法理解这些研讨会上公布的现代数学定义，更不用说检查它们的证明了。
数论在这方面的“落后”是我动手形式化现代FLT证明的主要动机之一。在项目完成之前，Lean将理解自同态形式和表示、Galois表示、潜在自同态性、模性提升定理、代数几何的算术、类域论、算术对偶性定理、Shimura簇等现代代数数论中使用的许多概念；形式化我自己领域内发生的事情的陈述将不再是科幻小说。那么，为什么要这么做呢？如果我们相信某些计算机科学家，那么AI的指数级增长最终应该会转化为计算机能够帮助数学家完成他们的工作。这样的工作可以帮助计算机理解我们在现代数学研究中正在做什么。
FLT项目
费马大定理形式化项目现已启动。比链接到github存储库更有趣的是蓝图图表，它显示了证明进度的指示。如果你是数学家，你可能也会对蓝图本身感兴趣，里面包含了我们将要采取的路径的进行中LaTeX写作，基本上是基于Richard Taylor的工作并在与我的讨论中发展出来的。Patrick Massot编写的蓝图软件是项目中至关重要的一部分，支持在形式化项目中进行大规模实时协作。对我们将要采取的路线的具体细节感兴趣的专家可以参考蓝图的第4章或我的2024年4月VaNTAGE研讨会(该研讨会将在5月初发布)。
EPSRC资助我项目的前五年。在此期间，我的首要目标是将FLT归结为1980年代末数学家已知的论断。我对我们能够成功实现这一目标持有相当的信心。但是“我们”是谁呢？
群众外包数学
我无法独自形式化FLT。事实上，在论证的几个部分，我理解基本原理，但从未仔细检查过细节，此外还有一些Langlands(GL2的循环基变换和Jacquet-Langlands)的非平凡输入，我只具备最表层的理解。然而，这正是形式化项目的好处之一。我将能够在Lean中明确陈述我需要的结果，并将其传递给其他人。系统的美妙之处在于：你不必理解FLT的整个证明就能做出贡献。蓝图将证明分解为许多小引理，如果你能形式化其中一个引理的证明，那么我将热切期待你的pull request。
该项目将在Lean Zulip聊天上的FLT频道运行，这是一个高水平的研究论坛，数学家和计算机科学家可以在实时协作中，使用线程和频道系统轻松发布代码和数学，这种系统能够出色地支持许多独立对话同时发生。对项目进展感兴趣的人可以偶尔查看蓝图图表；但对自己参与贡献感兴趣的人应该看看FLT频道上正在讨论的内容并表明身份。如果你想贡献力量，需要了解一些关于Lean的知识：如果你是想学习这种数学新表达方式的数学家，我推荐在线教材《Lean中的数学》。
我对这个项目将耗时多久没有任何感觉，但我肯定乐观地认为，在未来几年内我们可以证明一个现代的模性提升定理，从而将形式化FLT(一个1990年代的定理)的大项目简化为验证1980年代人类已知的结果。Lean的数学库将向上发展，我们将向下努力，最终我们将在中途相遇，届时计算机将真正理解费马大定理的证明。
本文译自 Lean community blog，由 BALI 编辑发布。