原文作者：Davide Castelvecchi
辅助证明软件能解决数学研究前沿的抽象理论问题，它们或将在数学中发挥更重要的作用。
Peter Scholz希望能够从一个基础理论开始，重构现代数学的许多内容。如今，Scholz构想的核心理论之一获得了意料之外的验证者：计算机。
尽管大部分数学家认为，他们工作的创造性方面在短期内不太可能被机器取代。但有些数学家承认，技术将在他们的研究中扮演日益重要的角色。而此次成功实践可能成为数学家开始接纳计算机辅助的转折点。
计算机成功验证了一个复杂的数学证明。
Scholze是德国波恩大学的数论学家。2019年，他与哥本哈根大学的Dustin Clausen一起，在波恩大学举办了一系列讲座，期间他们提出了一个雄心勃勃的计划——“凝聚态数学”（condensed mathematics）。他们表示，凝聚态数学将为从几何到数论的各个领域注入全新的理解，并在各领域间建立起联系。
其他学者对此颇为关注：Scholze被认为是数学界最耀眼的明星之一，曾提出过一些革命性的概念。霍普金斯大学的数学家Emily Riehl认为，如果Scholze和Clausen的构想得以实现，50年后研究生的数学教学方式将与今天截然不同。“我认为，许多数学领域在将来都会受到他的观点影响。”她说。 Peter Scholze，以算术代数几何而闻名的德国数学家。因“在代数几何学中发起的革命”，获得2018年菲尔兹奖，成为最年轻的菲尔兹奖得主之一。图片来源：https://www.quantamagazine.org
当时Scholze和Clausen大部分的构想都停留在一个十分复杂的数学证明上。证明过程是如此复杂，甚至连他们自己也不确定是否正确。但2021年6月的早些时候Scholze宣布，专用计算机软件帮助他成功检验了证明的核心部分。
计算机辅助
数学家使用计算机进行数值计算或者处理复杂方程已有很长时间。通过让计算机进行大量重复运算，他们已经证明了一些重要结论——最著名的例子便是上世纪70年代证明四色定理（只用四种颜色，就在任意地图上给任意两个相邻的国家着上不同的颜色）。
然而，一种称为证明助手（proof assistant）的系统功能更为深入。用户基于系统已知的简单对象，输入命题来使系统理解数学概念（一个对象）的定义。输入的命题可以只涉及已知对象，证明助手则会基于它现有的知识来判断该命题是“明显”正确或错误。如果证明助手的回答是不“明显”，用户则需要输入更多的信息来训练它。证明助手借此迫使用户更加严密地展开他们的论证逻辑，并填补数学家们有意无意省略的一些较简单步骤。
一旦研究人员完成了前期繁重的训练工作，使证明助手理解了一系列数学概念，系统就会生成一个计算机代码库。其他研究人员可以以此为基础进行研究，并定义更高级的数学对象。由此，证明助手就能够帮助检验那些耗时费力，甚至是人力所不可及的数学证明。
证明助手一直都不乏拥护者，但这是它首次在领域前沿发挥重要作用，帝国理工学院的数学家Kevin Buzzard说。他参与检验了Scholze和Clausen的研究结果。“之前遗留下来的一个重要问题是：证明助手能否处理复杂的数学问题？”Buzzard说。“我们证明了它们可以。”
而且这一切来得太快，超乎任何人的想象。2020年12月，Scholze向证明助手领域的专家们寻求帮助。德国弗赖堡大学的数学家Johan Commelin带领一队志愿者开始着手解决这一难题。五个多月后的2021年6月5日，Scholze就在Buzzard的博客中宣布，实验主体部分已经成功。“这简直不可思议。交互式证明助手现在已经达到了如此的高度：它能在合理时间内逻辑完备地验证复杂的原创研究。”Scholze写道。
Scholze和Clausen指出，凝聚态数学的关键在于重新定义现代数学的基石之一——拓扑（topology）的概念。数学家们研究的很多对象都具有拓扑。拓扑是对象的一种结构，它决定对象的哪些部分相连，哪些不是。拓扑提供了形状的信息，但是比起我们所熟悉的经典几何，拓扑更具延展性：在拓扑中，任意不分割对象的变换都是允许的。比如，一个三角形在拓扑上等价于其他任意三角形，甚至等价于圆形，但是无法等价于一条直线。
拓扑不仅在几何学，而且在泛函分析（functional analysis；一门研究函数的学科）中也发挥关键作用。函数空间通常是无穷维的（例如量子力学中基础的波函数）。另外，拓扑对于p进数（p-adic number）系统也非常重要，其具有一种与众不同的“分形”拓扑。
现代数学的大统一
2018年前后，Scholze和Clausen开始意识到，传统的拓扑定义方法导致了几何学、泛函分析和p进数三个数学领域之间存在兼容性问题，但新的基础概念或能弥合这些缺口。这三个领域明显各自处理的是截然不同的概念，但似乎会出现与另外两个领域中可类比的结果。两位学者提出，一旦拓扑能被“正确”定义，不同领域之间的相似结果就成了同一个“凝聚态数学”中的各个实例。这是三个领域的“某种大统一”，Clausen说。
Scholze和Clausen称，他们已经就一些重要几何事实发现了一些更简单、“凝聚”的证明，而且还能够证明一些之前未知的定理。这些研究尚未公之于众。
但还有一个问题。在纳入几何学之前，Scholze和Clausen还需要证明一个关于普通实数集直线拓扑结构的高度技术性的定理。Commelin解释说，“这像是一个基础定理，能将实数纳入这个新框架。”
用户基于证明助手包Lean中已有的较简单命题和概念，输入数学命题。在Scholze和Clausen的工作中，Lean输出了一个复杂的网络。图中各个命题被标注了不同的颜色并按照数学中的子领域分组。来源：Patrick Massot
Clausen回忆说，Scholze坚持不懈、夜以继日地工作，最终“凭借强大的意志”完成证明，在此过程中诞生了许多原创想法。“这是我见过的最惊人的数学成就。”他说。但是整个论证过于复杂，就连Scholze自己也担心有什么细微漏洞导致功亏一篑。“论证看起来很可信，但实在太过新颖。”Clausen说。
为了检查自己的工作，Scholze向数论学家Buzzard求助。Buzzard是助手软件包Lean的专家。Lean起初由微软研究院的一位计算机科学家发明，用于严格检查计算机代码中的错误。
Buzzard曾负责过一个为期数年的项目，项目内容是将帝国理工的所有本科数学课程编入Lean。他也曾试过将更高级的数学编入Lean，例如状似完备空间（perfectoid space）的概念。Scholze正是凭借这个理论赢得了2018年的菲尔兹奖。
另一位数论学家Commelin带队验证了Scholze和Clausen的证明。Commelin和Scholze决定将他们的Lean项目取名为“液体张力实验”（Liquid Tensor Experiment），以此向前卫摇滚乐队Liquid Tension Experiment致敬，因为他俩都是这个乐队的粉丝。
一场线上合作就此热火朝天地展开了。十多位精通Lean的数学家加入团队，研究人员还得到了计算机科学家们的协助。到六月初，这个团队已经将Scholze证明的核心部分（也是他最没有把握的部分）全部转译成了Lean代码。证明全部得以检验！该软件的确具有检验这部分数学证明的能力。
加深理解
Lean版本的Scholze的证明由成千上万行的代码组成，比原始版本长100多倍，Commelin说道。“如果单单看Lean的代码，尤其是当前版本的代码，你很难理解Scholze的证明。”但是研究者们说，将证明转换为代码在计算机里运行的整个过程，同样加深了他们对Scholze的证明的理解。
Riehl是试用过证明助手的数学家之一，她甚至在一些本科课程中教授相关内容。她说，虽然她没有在自己的研究中系统地使用这些工具，但是它们已经开始改变她的思考方式，关于如何构建数学概念、以及呈现和证明相关定理的做法。“以前我觉得证明和构建是两码事，但现在我认为它们是一样的。”
许多学者认为，短期内机器并不能代替数学家。证明助手读不懂数学课本，需要人类的持续输入，也不知道一个数学命题是否有趣或重要，它们只能判断命题正确与否，Buzzard说。但他补充说尽管如此，计算机或许马上就能够通过已知事实推导出被数学家们所忽视的结论了。
Scholze惊讶于证明助手的能力，但他不确定它们是否会继续在自己的研究中扮演重要角色。“目前看来，我并不清楚它们对我作为数学家的创造性工作会有什么帮助。”
原文以Mathematicians welcome computer-assisted proof in "grand unification’ theory为标题发表在2021年6月18日《自然》的新闻版块上
© nature
doi:10.1038/d41586-021-01627-2