跨越300多年的接力：受陶哲轩启发，数学家决定用AI形式化费马大定理的证明 https://www.jiqizhixin.com/articles/2024-05-03-4 机器之心 在陶哲轩的启发下，越来越多的数学家开始尝试利用 人工智慧 进行数学探索。 这次， 他们瞄准的目标是世界十大最顶尖数学难题之一的费马大定理。 费马大定理又称为「费马最後的定理（Fermat's Last Theorem，FLT）」，由17 世纪法 国数学家皮耶・德・费马提出。 它背後有一个传奇的故事。 据称，大约在1637 年左右 ，费马在阅读丢番图《 算术 》拉丁文译本时，曾在第11 卷第8 命题旁写道：「将一个 立方数分成两个立方数之和，或一个四次幂分成两个四次幂之和，或者一般地将一个高於 二次的幂分成两个同次方之和，这是不可能的。 这段话前面所表述的就是费马大定理的内容：当整数n>2 时，关於x^n + y^n=z^n 的方程 式没有正整数解。 费马表示，自己知道怎麽证明，但因为书的空白部分太小，所以没写。 对於该故事的真 实性以及费马是否真的想出了证明方法，後世是存在争议的。 在接下来的300 多年里，数学家一直在努力，接力证明费马大定理。 直到1995 年，美国 普林斯顿大学的Andrew Wiles 教授经过8 年的孤军奋战，终於用130 页长的篇幅完成了 证明。 Wiles 也成为整个数学界的英雄。 既然费马大定理已经被证明了，数学家还能用AI 做什麽？ 答案是：形式化它的证明。 数学的形式化通常指的是使用严格的形式语言（如 逻辑 和集合论）来表述数学对象、结 构、定理和证明，使其能够在计算机上进行表示、验证和操作，从而保证数学内容的准确 性和一致性。 去年年底，陶哲轩等人曾用Lean（一款互动式定理证明器，也是一门程式语言）形式化了 他们的一篇论文。 这篇论文是多项式Freiman-Ruzsa 猜想的一个版本的证明，於去年11 月发布在arXiv 上。 在写Lean 语言程式码的时候，陶哲轩也藉助了AI 程式设计助手 Copilot。 该事件引起数学界和 人工智慧 界的广泛关注。 当时，Lean 技术开源社群最重要的推广者、伦敦帝国学院的Kevin Buzzard 表示：「从 根本上来说，显而易见的是，当你将某些东西数位化时，你就可以以新的方式使用它。我 们将把数学数位化，这会让数学变得更好。 这位Buzzard 教授，就是最近宣称要形式化费马大定理证明的数学家，他所使用的工具也 是Lean。 在一篇部落格中，他介绍了自己做这件事情的背景、动机以及具体的做法。 为什麽要形式化费马大定理的证明？ 费马大定理的形式非常简洁、直观，然而证明它却异常艰难。 这无疑是数学深邃之美的 绝佳展示。 在过去的几个世纪中，为了解决这个问题，数学家们发展和创新了大量数学 理论，这些理论在密码学到物理学等多个领域都有所应用。 Andrew Wiles 可能因FLT 而受到启发，但他的工作实际上为朗兰兹计划带来了突破，该 计划是数学中一系列影响深远的构想，联系数论、代数几何与约化群表示理论，且在 2024 年依然备受瞩目。 历史上，代数数论的其他几个重大突破（例如数域中的 因式分解 理论和循环域的 算术 ）至少部分是出於对FLT 更深层理解的渴望。 Wiles 的工作，由他的学生Richard Taylor 一起补充完整，建立在20 世纪数学的庞大基 础之上。 Wiles 引入的基本技术——「模性提升定理（modularity lifting theorem） 」—— 在原始论文发表後的30 年间，在概念上被极大简化和广泛推广。 这一领域至今 仍然非常活跃。 Frank Calegari 在2022 年国际数学家大会上的论文，概述了自Wiles 突破以来的进展（参见：https://arxiv.org/abs/2109.14145）。 Kevin Buzzard 表示 ，这一领域的持续活跃，是他将FLT 证明形式化的动机之一。 数学的形式化，即将纸上的数学转换为能够理解定理和证明概念的电脑程式语言的艺术 。 这些程式语言，也称为互动式定理证明器（ITP），已经存在了数十年。 然而，近年 来，这一领域似乎吸引了数学界的一部分关注。 我们见证了多个研究数学形式化的例子 ，其中最新的是陶哲轩等人对多项式Freiman—Ruzsa 猜想证明的形式化。 这篇2023 年 的突破性论文在短短三周内就在Lean 中完成了形式化。 这样的成功案例可能会让旁观者 认为，像Lean 这样的ITP 现在已经准备好形式化所有现代数学了。 然而，真相远非如此简单。 在数学的某些领域，例如组合学，我们可以看到一些现代突 破可以即时形式化。 然而，Buzzard 表示，他定期参加伦敦数论研讨会，经常注意到 Lean 对现代数学定义的了解还不足以表达研讨会上宣布的结果，更不用说验证它们的证 明了。 事实上，数论在这一方面的「滞後」是Buzzard 启动FLT 当代证明形式化的主要动机之一 。 在专案完成之前，Lean 将能够理解自守形式（一类特别的复变数函数）和表示、伽罗 瓦表示、潜在自守性、模性提升定理、代数簇的 算术 、类域论、 算术 对偶定理、志村 簇等现代代数数论所使用的概念。 在Buzzard 看来，有了这些做基础，将他自己专业领 域正在发生的事情形式化将不再是科幻小说。 那麽，为什麽要这麽做呢？ Buzzard 解释说，「如果我们相信一些电脑科学家的话， 人 工智慧 的指数级增长终将使电脑能够帮助数学家进行研究。 这样的工作可以帮助电脑理 解我们在现代数学研究中正在做的事情。 」 项目如何开展？ 费马大定理的形式化计画现已启动。 Buzzard 在一幅图中展示了当前的进展。 有兴趣的研究者可以阅读详情： https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html 该计画由EPSRC 资助，Buzzard 将获得前五年的资金支持。 在此期间，他的第一个目标 是将FLT 简化为1980 年代末数学家已知的声明。 当然，Buzzard 没有打算独自完成这件事情。 他表示，对於有些论证的部分，他理解其 基本原则，但从未仔细检查过细节。 而且，朗兰兹计划还引入了一些重要的东西，包括 GL_2 的循环基变换以及Jacquet-Langlands。 对於这些深奥的东西，他的理解还不够深 。 不过，这恰恰是形式化计画的优势所在。 Buzzard 将能够在Lean 中明确表述他需要的结 果，并将它们传递给其他人。 这个系统的美妙之处在於：你不必理解FLT 的整个证明就 能做出贡献。 上面的图将证明分解为许多小引理，因此非常方便进行众包操作。 如果你 能形式化证明其中任何一个引理，那麽Buzzard 会热切期待你的拉取请求。 想要参与专案的人需要了解一些关於Lean 的知识。 对此，Buzzard 推荐了线上教科书 Mathematics in Lean。 教科书连结：https://leanprover-community.github.io/mathematics_in_lean/ 该计画将在Lean Zulip chat 的FLT stream 上进行，这是一个强大的研究论坛，数学家 和电脑科学家可以即时协作，轻松地发布程式码和数学，使用线程和stream 系统，有效 地支援多场独立对话同时进行。 Lean Zulip chat 连结：https://leanprover.zulipchat.com/ Buzzard 表示，他对这个计画将需要多长时间没有任何预感，但他绝对乐观。 同时，像Lean 这类形式化证明工具也在不断迭代。 相较於初代Lean，现在最新的Lean 4 版本进行了多项最佳化，包括更快的编译器、改进的错误处理和更好的与外部工具整合 的能力等。 去年年底，开放平台LeanDojo 团队和加州理工学院的研究者也推出了Lean Copilot，这 是一款专为大型 语言模型 与人类互动而设计的协作工具，为数学研究注入了AI 大模型 的力量。 「我预计，如果使用得当，到2026 年，AI 将成为数学研究和许多其他领域值得信赖的合 着者。」陶哲轩在之前的部落格中说道。 希望陶哲轩的预言早日成真。 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 114.38.27.129 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1714741883.A.73A.html