报告人：伦敦帝国理工学院KevinBuzzard（凯文·巴扎德）教授
演讲前言：
为普通数学家讲授证明形式化。摘要：形式主义是把你真正的意思写下来的艺术。数学有着丰富的形式化历史：欧几里德、罗素-怀特海和布尔巴基都曾尝试过。本世纪，Avigad、Hales和Gonthier向我们展示了另一种方式。现在，新一代的年轻人正在将代数、分析、范畴论、组合数学、几何、数论、拓扑学等形式化，这一次他们使用的是计算机。Lean的数学库mathlib包含近百万行免费开放源代码，对应于80000多个定理的证明，如伽罗瓦Galois理论的基本定理，并且它正在快速增长。接受过数学库训练的AI已经自己解决了国际数学奥林匹克IMO问题。正在发生什么？这不是为了确保论文是正确的。这并不是要制作一个只使用数学公理就可以打印出BSD猜想（Birch和Swinnerton-Dyer）的十亿行证明的计算机程序。这不是从证明中提取美，只留下有向无环图。这是关于开发有潜力以新方式帮助研究人员和博士生的计算机工具。仍有许多工作要做。我将对该领域进行概述。
演讲PPT正文：
数学形式主义的兴起。
KevinBuzzard，伦敦帝国理工学院
2022年7月9日，国际数学家大会
在我们开始之前
感谢主办方的邀请，感谢大家的光临！
数学和计算机
60年来，计算机在计算方面一直优于人类。
25年来，它们在国际象棋上一直比我们好。
几年来，他们的表现比我们好。
他们什么时候会比我们更擅长证明定理？
nature自然杂志的两篇报道截图
·数学家欢迎对“大统一”理论的计算机辅助证明
·DeepMind的AI帮助解开纽结的数学
结局的开始？
在证明研究级数学定理方面，计算机很快会比人类更好吗？
我们作为数学研究人员的工作是否处于危险之中？
不。（在我看来）。
开始的开始。
然而，计算机会很快帮助人类证明定理吗？
不仅仅是通过举例，而是通过推理？
在数据库中寻找证明或反例，自己构建简单的证明，进行图解表示的追寻？
计算机会让人类更容易学习数学吗？
它们会让人类以新的方式探索证据吗？
我的猜测：是的。
谈话概要
计算机定理证明器的现场演示
该领域的一些历史
最先进的技术
如何参与
计算机证明助手是啥？
我们即将看到Lean在行动。
存在许多其他这样的系统（Coq、Isabelle/HOL、HOLLight、Agda、cubicalAgda、Metamath、Mizar......）。
您可以使此此类系统来形式化数学证明。
还有自动定理证明器，如Prover9、Otter、E、Waldmeister、Vampire...
我们刚刚看到了什么？
我们都知道计算机可以用来计算。
我们刚刚看到它们现在可以用来推理。
证明助手：将数学问题变成电脑益智游戏的关卡。
我们刚刚看到他们在做本科层次的拓扑。
这些东西只是玩具吗？
历史（2000年份以前）
1970年代：第一个经过计算机验证的实数构造为一个完备的有序域（Jutting的论文）。
1990年代：系统可以检查人类输入的简单定理证明（本科阶段）。
历史（21世纪）
2000年代的一些里程碑：
2004年：Avigad等人在Isabelle/HOL中正式验证了素数定理（还有Harrison2009在HOLLight中）。
2004年：Gonthier正式验证了四色定理。
2005年：Hales在Isabelle/HOL中正式验证了Jordan曲线定理。
2013：Gonthier等正正式验证了Coq中的奇数阶定理。
数学界的反应很少。
我希望我今天要谈论的结果会引起更大的反响。
开普勒猜想
1998年，海尔斯（Hales）和弗格森（Ferguson）证明了开普勒猜想（3维球体堆积的最佳密度）。
部分证明涉及在计算机上检查23000个非线性不等式。（请注意，（本次大会刚获得菲尔兹奖的Viazovska）在8维和24维中的工作更具概念性）。
五年后，《数学年鉴》告诉海尔斯，裁判员无法完全证明这一证明。
Hales的非凡反应：他组建了一个由20多人组成的团队，并在接下来的12年中，在交互式定理证明器中将结果形式化。
他们在2015年取得了成功。
海尔斯的结论
海尔斯，现在是该领域的专家，在牛顿研究所发表讲话关于2017年7月的故事。
他得出的结论是，以下项目现在是可行的：
创建一个系统，该系统能够理解当前在严肃的纯数学期刊上发表的所有定理的陈述。
陈述比证明更容易！
陈述是必要的第一步。
如果计算机甚至无法理解问题，它们如何帮助我们找到答案？
比看起来更难
要形式化2022研究级数学的陈述，我们最好先形式化完整的本科学位内容。
如果你的证明器中没有光滑流形、向量丛、类群以及各种基本同调和上同调理论（奇异上同调、deRham上同调……）的定义，那么你有什么机会呢？
因为我们的社区在很大程度上对这项工作不感兴趣，所以2017年没有一个系统有这些定义。这是我们的错。
更近期的历史
2017年，我在伦敦帝国理工学院创办了一个名为XenaProject的Lean俱乐部。
目标是(a)教本科生如何使用该软件，以及(b)将我们本科课程的部分内容形式化。
学生们很快就想承担有限群论的项目，然后是更雄心勃勃的项目。
Lean社区欢迎我们加入并教我们如何使用该软件。
他们邀请我们帮助建立一个Lean数学库，称为mathlib。
本科数学家定义了线性映射、矩阵、子群、...并将它们添加到Lean的数学库中。
概型
在1960年代，格罗滕迪克（Grothendieck）通过引入概型（Scheme）的概念彻底改变了代数几何。
2018年，我和俱乐部的一些本科生（KennyLau、ChrisHughes、AmeliaLivingston、RamonFernándezMir）在Lean中定义了概型。
然后我们开始在Hartshorne的代数几何教科书中做练习。
这比你想象的要难，但也不是太难。
Lean社区鼓励我们发布（我们这样做了，斯科特·莫里森（ScottMorrison）使用“范畴”语言重新定义了所有内容）。
但是我们仍然需要更多的东西来打动数学家。
完美空间
2018年，彼得·舒尔茨（PeterScholze）获得菲尔兹奖。
有部分原因是他关于完美空间（Perfectoidspaces）的工作。
2019年，JohanCommelin、PatrickMassot和我本人在Lean中形式化定义了完美空间。
为什么我们要形式化完美空间？
一种使用软件的新方法（关于复杂对象的简单定理，而不是关于简单对象的复杂定理）。
检查现代计算机证明系统是否可以处理如此复杂的定义。
一种正确学习定义的有趣方式。
宣传噱头。
但它奏效了：它使该领域引起了更多数学家的注意。
Lean不是我
Lean不是我“KevinBuzzard的项目”，它的数学库也不是。
Lean的数学库mathlib是一个巨大的合作项目。
这是一个庞大的本科数学数据库，由数百名志愿者建立，由Lean证明器社区领导，我只是其中的一小部分。
最近的项目
现在，我将快速浏览定理证明器社区中大家最近一直在做的一些数学列表，主要是在研究所水平。
液体张量实验
2020年12月，PeterScholze向定理证明器社区发起挑战，以验证液
体向量空间的基本定理（由Clausen和Scholze证明）：
对于i≥1,有
这是关于凝聚阿贝尔群范畴中更高维推广的技术结果。
六个月后，由JohanCommelin领导的团队在Lean中形式化了Scholze认为是问题核心的关键技术引理的证明。
社区（Commelin、Topaz和许多其他人）即将完成这项工作。
我们从这项工作中学到了什么？
首先，Commelin大大简化了Clausen-Scholze证明的一部分（“Commelin复形”）。
其次，Scholze声称这段经历教会了他“究竟是什么让证明有效”。
“...这让我意识到，实际上发生的关键事情是将实数上的非凸问题简化为整数上的凸问题。”
第三，我们看到系统现在可以处理复杂对象的复杂证明。
2013年：VladimirShchur证明了格罗莫夫双曲空间的莫尔斯引理的定量版本。
证明发表在《泛函分析杂志》上。
SébastienGouzel试图在Isabelle/HOL中将结果形式化，但发现了一个根本错误。
Gouzel和Shchur发现了一个新的（更复杂的）证明。
2018年：（他们的）联合论文，具有更好的估计，以及完全形式化的证明。
2016年：Ellenberg和Gijswijt解决了CapSet帽集猜想（仿射几何中，三元域上的n维仿射空间的最大子集，没有3个元素处于同一条线上）。
该工作发表在《数学年鉴》上。
2019年，Dahmen、Hlzl和Lewis在Lean中形式化了证明。
2021年12月：ThomasBloom证明了一个具有正上密度的集合包含一个有限子集S，满足子集中全部元素倒数和为1
这个结论回答了两位已故著名数学家Erds（厄尔多斯）和Graham（葛立恒，又译格雷厄姆）的一个问题。
他然后通过BhavikMehta（1998年菲尔兹奖获得者、《普林斯顿数学指南》作者剑桥大学Gowers高尔斯爵士的一个博士生）学会了如何使用Lean。
6个月后，Bloom和Mehta在Lean中完全形式化了这个证明。
这项工作包含Hardy-Littlewood（哈代-李特伍德）圆法的一个实例的形式化。
Bloom的论文目前仍在被审阅中。
2021年：Baanen、Dahmen、Narayanan和Nuccio在Lean中形式化了戴德金Dedekind域和相应类群。
他们还形式化了整体域的类群是有限的这一证明。
2022年：deFrutosFernández在Lean中形式化了整体域上的adeles和ideles。
她证明了idele类群与ideal理想类群之间的关系。
SebastianMonnet在Galois群上正式定义了Krull拓扑，并证明它是有限的。
deFrutosFernández接着以非上同调的形式陈述了整体类域论的主要猜想。
在过去的几个月里，Livingston定义了群上同调和伽罗瓦上同调。
她目前正在研究表达局部和整体定理的上同调形式。
DeFrutosFernandez概述了一种形式化局部类域论主要定理证明的方法，这是自然而然的下一个项目。
Narayanan目前正在研究Iwasawa理论。
她已经定义了p进L-函数，并且目前正在证明它们的特殊值与广义伯努利数有关。
Gouzel、Kudryashov、Macbeth、Degenne和Ying已经在Lean中将分析和概率形式化。
最近取得的显著成果有大数定律、多变量微积分中的变量变化、勒贝格微分定理、柯西积分定理以及鞅（martingales）的定义和基本性质。
2020年，Commelin和Lewis将交换环R的Witt向量环W(R)形式化。
利用他们的工作，deFrutosFernández正在研究Fontaine环的定义，例如B_{dR}
自然的下一步：分幂理想和B_{cris}。
同样在p进霍奇（p-adicHodge）理论中：Dupuis、Lewis和Macbeth在具有正特征的代数闭域上对一维等晶体进行了分类。
1999年：WarwickTucker证明洛伦兹Lorenz吸引子是混沌的。
Tucker的证明涉及大量用C++编写的计算。
2017年，Immler使用Isabelle/HOL完成了计算的形式验证。
ScottMorrison建立了一个巨大的范畴理论库（基、幺半范畴等）。
Commelin、Himmel、Morrison、Topaz和Yang使用它建立了阿贝尔范畴、导函子和同调代数。
（这对于液体张量实验是必不可少的）。
Nash纳什在Lean中将李代数形式化，并在此过程中提出了似乎是Engel恩格尔定理的一个新的、更具概念性的证明。
2022年:JujianZhang在Lean中对射影概型（projectiveschemes）形式化，目前正在定义层上同调（sheafcohomology）。étale上同调绝对是即将出现的（底层的交换代数也处于有利阶段）。
我在Lean中定义了椭圆曲线，Birkbeck定义了模形式并陈述了模猜想。
Karatarakis和我正在慢慢地开始寻找证明的旅程。这将需要很多很多人年。是否需要很多年，很大程度上取决于参与的人数。
与此同时，Brasca正在领导一个项目，对正则素数（regularprimes），将费马大定理的旧证明形式化。
你可以通过查看依赖关系图来监控进度。
1978年:Apéry证明了ζ(3)是无理数。
2019年，Mahboubi和Sibut-Pinote（他们与Chyzak和Tassi的早期工作之后）在Coq中形式化了证明。
2019年：ManuelEberl在Isabelle/HOL正式确定了Apostol解析数论书中的绝大部分内容。
他所做的例子：黎曼假设的陈述，以及关于算术级数中素数的狄利克雷定理的证明。
2021年：Bordg、Paulson和Li在Isabelle/HOL中形式化概型（scheme）的定义。
（出于基础原因很有趣）
Mehta和Dillies在Lean中形式化了Szemerédi的正则引理和Roth的算术级数定理，而Edmonds、Koutsoukou-Argyraki和Paulson在Isabelle/HOL中形式化了相同的结果。
以前的许多项目都有数论或代数的味道。
这仅仅反映了定理证明器社区内数学家的兴趣。
Massot、vanDoorn和Nash的球体外翻项目是一个完全不同领域的非平凡的项目。
球体外翻项目
定理（斯梅尔Smale，50年代）：球体可以外翻。
真的有可能在计算机定理证明器中形式化这样的结果吗？
Massot观察到应该形式化的是格罗莫夫Gromov的h原理，通过凸积分。
你可以在这里看到他们目前的进展。
加入
许多现代定理证明器在Discord或Zulip上有在线社区。例如：
·Coq:coq.zulipchat.com
·Lean:leanprover.zulipchat.com
·Isabelle:isabelle.zulipchat.com
·Agda:agda.zulipchat.com
未来
他们将音乐（CD、MP3）数字化，但当时没有人预见到后果（Napster、Spotify）。