小乐数学科普：2022国际数学家大会一小时报告《数学形式主义的兴起》Kevin Buzzard 演讲全文

编者按：形式主义，作为数学历史中三大主义流派之一，经历过多次跌宕起伏，而如今随着人工智能、机器学习的兴起以及开源社区的共同努力，用计算机做奥数题、检查数学证明过程是否有误、甚至自动发现和形式化证明数学定理，在理论和实践中又会碰撞出什么火花，又会如何囿于哥德尔不完全定理。Kevin Buzzard教授在2022本届国际数学家大会一小时报告演讲中提供了一些信息和思考见解供各位参考（另请参阅zzllrr小乐之前编译的量子杂志对Kevin Buzzard的采访播客内容，以及Lean的介绍）

时间：2022-7-9 周六 Special Plenary Lecture特别大会报告

报告人：伦敦帝国理工学院Kevin Buzzard（凯文·巴扎德）教授

演讲前言：

为普通数学家讲授证明形式化。摘要：形式主义是把你真正的意思写下来的艺术。数学有着丰富的形式化历史：欧几里德、罗素-怀特海和布尔巴基都曾尝试过。本世纪，Avigad、 Hales和 Gonthier向我们展示了另一种方式。现在，新一代的年轻人正在将代数、分析、范畴论、组合数学、几何、数论、拓扑学等形式化，这一次他们使用的是计算机。Lean的数学库mathlib包含近百万行免费开放源代码，对应于80000多个定理的证明，如伽罗瓦Galois理论的基本定理，并且它正在快速增长。接受过数学库训练的AI已经自己解决了国际数学奥林匹克IMO问题。正在发生什么？这不是为了确保论文是正确的。这并不是要制作一个只使用数学公理就可以打印出BSD猜想（Birch和Swinnerton-Dyer）的十亿行证明的计算机程序。这不是从证明中提取美，只留下有向无环图。这是关于开发有潜力以新方式帮助研究人员和博士生的计算机工具。仍有许多工作要做。我将对该领域进行概述。

演讲PPT正文：

数学形式主义的兴起。

Kevin Buzzard，伦敦帝国理工学院

2022年7月9日，国际数学家大会

在我们开始之前

感谢主办方的邀请，感谢大家的光临！

数学和计算机

60 年来，计算机在计算方面一直优于人类。

25 年来，它们在国际象棋上一直比我们好。

几年来，它们的表现比我们好。

它们什么时候会比我们更擅长证明定理？

nature自然杂志的两篇报道截图

    ·数学家欢迎对“大统一”理论的计算机辅助证明

    ·DeepMind的AI帮助解开纽结的数学

结局的开始？

在证明研究级数学定理方面，计算机很快会比人类更好吗？

我们作为数学研究人员的工作是否处于危险之中？

不。（在我看来）。

开始的开始。

然而，计算机会很快帮助人类证明定理吗？

不仅仅是通过举例，而是通过推理？

在数据库中寻找证明或反例，自己构建简单的证明，进行图解表示的追寻？

计算机会让人类更容易学习数学吗？

它们会让人类以新的方式探索证据吗？

我的猜测：是的。

谈话概要

•     计算机定理证明器的现场演示

•     该领域的一些历史

•     最先进的技术

•     如何参与

计算机证明助手是啥？

我们即将看到Lean在行动。

存在许多其他这样的系统（Coq、Isabelle/HOL、HOL Light、Agda、cubical Agda、Metamath、Mizar ......）。

您可以使用此类系统来形式化数学证明。

还有自动定理证明器，如 Prover9、Otter、E、Waldmeister、Vampire ...

https://gitpod.io/#https://github.com/leanprover-community/mathlib

我们刚刚看到了什么？

我们都知道计算机可以用来计算。

我们刚刚看到它们现在可以用来推理。

证明助手：将数学问题变成电脑益智游戏的关卡。

我们刚刚看到它们在做本科水平的拓扑。

这些东西只是玩具吗？

历史（2000年份以前）

1970 年代：第一个经过计算机验证的实数构造为一个完备的有序域（Jutting 的论文）。

1990 年代：系统可以检查人类输入的简单定理证明（本科阶段）。

历史（21世纪）

2000 年代的一些里程碑：

• 2004 年：Avigad 等人在 Isabelle/HOL 中正式验证了素数定理（还有 Harrison 2009 在 HOL Light 中）。

• 2004 年：Gonthier 正式验证了四色定理。

• 2005 年：Hales 在 Isabelle/HOL 中正式验证了 Jordan 曲线定理。

• 2013：Gonthier 等正式验证了 Coq 中的奇数阶定理。

数学界的反应很少。

我希望我今天要谈论的结果会引起更大的反响。

开普勒猜想

1998 年，海尔斯（Hales）和弗格森（Ferguson）证明了开普勒猜想（3 维球体堆积的最佳密度）。

部分证明涉及在计算机上检查 23000 个非线性不等式。（请注意，（本次大会刚获得菲尔兹奖的Viazovska） 在 8 维和 24 维中的工作更具概念性）。

五年后，《数学年鉴》告诉海尔斯，审稿人无法完全证明这一证明。

Hales 的非凡反应：他组建了一个由 20 多人组成的团队，并在接下来的12 年中，在交互式定理证明器中将结果形式化。

他们在 2015 年取得了成功。

海尔斯的结论

海尔斯，现在是该领域的专家，在牛顿研究所发表关于 2017 年 7 月的故事。

https://www.newton.ac.uk/seminar/21474/

https://api.newton.ac.uk/website/v0/seminars/21474/presentation-files/250

他得出的结论是，以下项目现在是可行的：

创建一个系统，该系统能够理解当前在严肃的纯数学期刊上发表的所有定理的陈述。

陈述比证明更容易！

陈述是必要的第一步。

如果计算机甚至无法理解问题，它们如何帮助我们找到答案？

比看起来更难

要形式化2022研究级数学的陈述，我们最好先形式化完整的本科学位内容。

如果你的证明器中没有光滑流形、向量丛、类群以及各种基本同调和上同调理论（奇异上同调、de Rham 上同调……）的定义，那么你有什么机会呢？

因为我们的社区在很大程度上对这项工作不感兴趣，所以2017年没有一个系统有这些定义。这是我们的错。

更近期的历史

2017 年，我在伦敦帝国理工学院创办了一个名为 Xena Project 的Lean俱乐部。

目标是 (a) 教本科生如何使用该软件，以及 (b) 将我们本科课程的部分内容形式化。

学生们很快就想承担有限群论的项目，然后是更雄心勃勃的项目。

Lean社区欢迎我们加入并教我们如何使用该软件。

他们邀请我们帮助建立一个Lean数学库，称为 mathlib。

本科数学工作者定义了线性映射、矩阵、子群、...并将它们添加到Lean 的数学库中。

概型

在 1960 年代，格罗滕迪克（Grothendieck）通过引入概型（Scheme）的概念彻底改变了代数几何。

2018 年，我和俱乐部的一些本科生（Kenny Lau、Chris Hughes、Amelia Livingston、Ramon Fernández Mir）在Lean中定义了概型。

然后我们开始在 Hartshorne 的代数几何教科书中做练习。

这比你想象的要难，但也不是太难。

Lean社区鼓励我们发布（我们这样做了，斯科特·莫里森（Scott Morrison）使用“范畴”语言重新定义了所有内容）。

但是我们仍然需要更多的东西来打动数学家。

完美空间

2018 年，彼得·舒尔茨（Peter Scholze）获得菲尔兹奖。

有部分原因是他关于完美空间（Perfectoid spaces）的工作。

2019 年，Johan Commelin、Patrick Massot 和我本人在Lean中形式化定义了完美空间。

为什么我们要形式化完美空间？

• 一种使用软件的新方法（关于复杂对象的简单定理，而不是关于简单对象的复杂定理）。

• 检查现代计算机证明系统是否可以处理如此复杂的定义。

• 一种正确学习定义的有趣方式。

• 宣传噱头。

但它奏效了：它使该领域引起了更多数学家的注意。

Lean不是我

Lean不是我“Kevin Buzzard的项目”，它的数学库也不是。

Lean 的数学库 mathlib 是一个巨大的合作项目。

这是一个庞大的本科数学数据库，由数百名志愿者建立，由Lean证明器社区领导，我只是其中的一小部分。

最近的项目

现在，我将快速浏览定理证明器社区中大家最近一直在做的一些数学列表，主要是在研究生水平。

液体张量实验

2020 年 12 月，Peter Scholze 向定理证明器社区发起挑战，以验证液

体向量空间的基本定理（由 Clausen 和 Scholze 证明）：

对于i≥1,有

这是关于凝聚阿贝尔群范畴中更高维推广的技术结果。

六个月后，由 Johan Commelin 领导的团队在 Lean 中形式化了 Scholze 认为是问题核心的关键技术引理的证明。

社区（Commelin、Topaz 和许多其他人）即将完成这项工作。

我们从这项工作中学到了什么？

首先，Commelin 大大简化了 Clausen-Scholze证明的一部分（“Commelin 复形”）。

其次，Scholze 声称这段经历教会了他“究竟是什么让证明有效”。

“. . .这让我意识到，实际上发生的关键事情是将实数上的非凸问题简化为整数上的凸问题。”

第三，我们看到系统现在可以处理复杂对象的复杂证明。

---

2013 年：Vladimir Shchur 证明了格罗莫夫双曲空间的莫尔斯引理的定量版本。

证明发表在《泛函分析杂志》上。

Sébastien Gouëzel 试图在 Isabelle/HOL 中将结果形式化，但发现了一个根本错误。

Gouëzel 和 Shchur 发现了一个新的（更复杂的）证明。

2018年：（他们的）联合论文，具有更好的估计，以及完全形式化的证明。

---

2016 年：Ellenberg 和 Gijswijt 解决了 Cap Set帽集猜想（仿射几何中，三元域上的n维仿射空间的最大子集，没有3个元素处于同一条线上）。

https://en.wikipedia.org/wiki/Cap_set 

该工作发表在《数学年鉴》上。

2019 年，Dahmen、Hölzl 和 Lewis 在 Lean中 形式化了证明。

---

2021 年 12 月：Thomas Bloom证明了一个具有正上密度的集合包含一个有限子集S，满足子集中全部元素倒数和为1

这个结论回答了两位已故著名数学家Erdös（厄尔多斯）和Graham（葛立恒，又译格雷厄姆）的一个问题。

他然后通过Bhavik Mehta（1998年菲尔兹奖获得者、《普林斯顿数学指南》作者剑桥大学Gowers高尔斯爵士的一个博士生）学会了如何使用Lean。

6个月后，Bloom和Mehta在Lean中完全形式化了这个证明。

这项工作包含Hardy-Littlewood（哈代-李特伍德）圆法的一个实例的形式化。

Bloom的论文目前仍在被审阅中。

---

2021 年：Baanen、Dahmen、Narayanan 和 Nuccio 在Lean中形式化了戴德金Dedekind域和相应类群。

他们还形式化了整体域的类群是有限的这一证明。

2022 年：de Frutos Fernández 在Lean中形式化了整体域上的adeles和ideles。

她证明了idele类群与ideal理想类群之间的关系。

Sebastian Monnet 在 Galois 群上正式定义了 Krull 拓扑，并证明它是有限的。

de Frutos Fernández 接着以非上同调的形式陈述了整体类域论的主要猜想。

---

在过去的几个月里，Livingston定义了群上同调和伽罗瓦上同调。

她目前正在研究表达局部和整体定理的上同调形式。

De Frutos Fernandez 概述了一种形式化局部类域论主要定理证明的方法，这是自然而然的下一个项目。

Narayanan 目前正在研究 Iwasawa 理论。

她已经定义了 p 进 L-函数，并且目前正在证明它们的特殊值与广义伯努利数有关。

Gouëzel、Kudryashov、Macbeth、Degenne 和 Ying 已经在Lean中将分析和概率形式化。

最近取得的显著成果有大数定律、多变量微积分中的变量变化、勒贝格微分定理、柯西积分定理以及鞅（martingales）的定义和基本性质。

---

2020 年，Commelin 和 Lewis 将交换环 R 的 Witt向量环 W(R) 形式化。

利用他们的工作，de Frutos Fernández 正在研究 Fontaine环的定义，例如B_{dR}

自然的下一步：分幂理想和B_{cris}。

同样在p进霍奇（p-adic Hodge）理论中：Dupuis、Lewis 和 Macbeth 在具有正特征的代数闭域上对一维等晶体进行了分类。

---

1999 年：Warwick Tucker 证明洛伦兹Lorenz吸引子是混沌的。

Tucker 的证明涉及大量用 C++ 编写的计算。

2017 年，Immler 使用 Isabelle/HOL 完成了计算的形式验证。

Scott Morrison 建立了一个巨大的范畴理论库（基、幺半范畴等）。

Commelin、Himmel、Morrison、Topaz 和 Yang 使用它建立了阿贝尔范畴、导函子和同调代数。

（这对于液体张量实验是必不可少的）。

Nash纳什在Lean中将李代数形式化，并在此过程中提出了似乎是Engel恩格尔定理的一个新的、更具概念性的证明。

---

2022 年: Jujian Zhang 在Lean中对射影概型（projective schemes）形式化，目前正在定义层上同调（sheaf cohomology）。Étale 上同调绝对是即将出现的（底层的交换代数也处于有利阶段）。

我在 Lean 中定义了椭圆曲线，Birkbeck 定义了模形式并陈述了模猜想。

Karatarakis 和我正在慢慢地开始寻找证明的旅程。这将需要很多很多人年。是否需要很多年，很大程度上取决于参与的人数。

与此同时，Brasca 正在领导一个项目，对正则素数（regular primes），将费马大定理的旧证明形式化。

你可以通过查看依赖关系图来监控进度。

https://leanprover-community.github.io/flt-regular/dep_graph_document.html

1978年: Apéry 证明了 ζ(3)是无理数。

2019 年，Mahboubi 和 Sibut-Pinote（他们与 Chyzak 和 Tassi 的早期工作之后）在 Coq 中形式化了证明。

---

2019 年：Manuel Eberl 在 Isabelle/HOL 正式确定了 Apostol解析数论书中的绝大部分内容。

他所做的例子：黎曼假设的陈述，以及关于算术级数中素数的狄利克雷定理的证明。

2021 年：Bordg、Paulson 和 Li 在 Isabelle/HOL 中形式化概型（scheme）的定义。

（出于基础原因很有趣）

Mehta 和 Dillies 在 Lean 中形式化了 Szemerédi 的正则引理和Roth 的算术级数定理，而Edmonds、Koutsoukou-Argyraki 和Paulson 在 Isabelle/HOL 中形式化了相同的结果。

---

以前的许多项目都有数论或代数的味道。

这仅仅反映了定理证明器社区内数学家的兴趣。

Massot、van Doorn 和 Nash 的球体外翻项目是一个完全不同领域的非平凡的项目。

球体外翻项目

定理（斯梅尔Smale，50 年代）：球体可以外翻。

网上有视频可视化地展示了构造。https://youtu.be/OI-To1eUtuU?t=95

真的有可能在计算机定理证明器中形式化这样的结果吗？

Massot 观察到应该形式化的是格罗莫夫Gromov 的 h 原理，通过凸积分。

你可以在这里看到他们目前的进展。

https://leanprover-community.github.io/sphere-eversion/blueprint/index.html

加入

一个有趣的起点是写给我大学的本科生的自然数游戏。https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

许多现代定理证明器在 Discord 或 Zulip 上有在线社区。例如：

• Coq: coq.zulipchat.com

• Lean: leanprover.zulipchat.com

• Isabelle: isabelle.zulipchat.com

• Agda: agda.zulipchat.com

未来

他们将音乐（CD、MP3）数字化，但当时没有人预见到后果（Napster、Spotify）。

我们正在数字化数学，我相信这将不可避免地改变数学。

欢迎您加入我们。

非常感谢您的关注。

---

• 点击左下角“阅读原文”，查看原始文章出处。

• 点击“zzllrr小乐”公众号主页，右上角“设为星标”，数学科普不迷路。