用计算机来验证一个复杂的数学证明的努力已经成功了。资料来源:法德尔·塞纳/法新社，盖蒂报道
彼得·肖尔兹(peter Scholze)希望从现代数学的基石之一开始，重建现代数学的大部分内容。现在，他已经从一个不太可能的来源获得了验证，证明他的探索的核心:一台电脑。
尽管大多数数学家怀疑机器会很快取代他们职业中的创造性方面，但一些人承认技术将在他们的研究中发挥越来越重要的作用——而这一特殊的成就可能是接受它的转折点。
肖尔策是一名数字理论家，他在2019年他所在的德国波恩大学的一系列讲座中提出了这一雄心勃勃的计划，该计划是他与哥本哈根大学的合作者达斯汀·克劳森共同创建的。两位研究人员称其为“浓缩数学”，他们表示，它有望为从几何学到数论等领域带来新的见解和联系。
其他研究人员也在关注这个问题:Scholze被认为是数学领域最耀眼的明星之一，在引入革命性概念方面有着良好的记录。马里兰州巴尔的摩市约翰霍普金斯大学的数学家Emily Riehl说，如果Scholze和Clausen的设想得以实现，50年后教授研究生数学的方式将与现在大不相同。她说:“我认为未来数学的很多领域都将受到他的思想的影响。”
到目前为止，这一设想的大部分都依赖于技术证据，以至于Scholze和Clausen都不能确定它是否正确。但是这个月的早些时候，Scholze宣布一个使用专业计算机软件检查证明核心的项目已经成功。
电脑帮助数学家们长期以来一直使用计算机进行数值计算或处理复杂的公式。在某些情况下，他们通过让计算机做大量重复性工作来证明主要成果——最著名的例子是在20世纪70年代证明了任何地图都可以只用四种不同的颜色着色，而不用用同一颜色填充任何两个相邻的国家。
数论天才是最令人垂涎的数学奖得主之一
但被称为证据助手的系统更深入。用户向系统输入语句，教它一个数学概念的定义——一个对象——基于机器已经知道的更简单的对象。一个陈述也可以仅指已知的对象，而证明助手将根据其现有知识回答该事实是“明显的”正确还是错误。如果答案不明显，用户必须输入更多的细节。因此，证明助手迫使用户以一种严格的方式展示他们的论点的逻辑，他们填补了人类数学家有意识或无意识跳过的更简单的步骤。
一旦研究人员完成了将一组数学概念转化为证明助手的艰巨工作，该程序就会生成一个计算机代码库，其他研究人员可以在此基础上构建这些代码库，并用于定义更高层次的数学对象。通过这种方式，证明助手可以帮助验证数学证明，否则将是耗时和困难的，甚至可能是实际上不可能的，一个人来检查。
证明助手早就有了自己的粉丝，但这是他们第一次在一个领域的前沿发挥重要作用，凯文·布扎德说，他是伦敦帝国理工学院的数学家，参与了检查Scholze和Clausen的结果的合作。“剩下的最大问题是:它们能处理复杂的数学吗?”卑鄙的小人说。“我们证明了他们可以做到。”
这一切发生得比任何人想象的都要快。2020年12月，Scholze向证明助理专家提出了他的挑战，德国弗莱堡大学(University of Freiburg)数学家约翰·科梅林(Johan Commelin)领导的一组志愿者接受了挑战。6月5日，不到6个月后，Scholze在Buzzard的博客上发帖称，实验的主要部分已经成功。Scholze写道:“我觉得这绝对是疯狂的，交互式证明助手现在达到了这样的水平，在非常合理的时间跨度内，他们可以正式验证困难的原始研究。”
人工智能数学天才为人类创造棘手的新问题
根据Scholze和Clausen的观点，浓缩数学的关键在于重新定义拓扑的概念，拓扑是现代数学的基石之一。数学家研究的很多物体都有一个拓扑结构——一种结构，它决定了物体的哪些部分靠近，哪些不靠近。拓扑学提供了一个形状的概念，但它比那些熟悉的、学校级别的几何更有可塑性:在拓扑学中，任何不能将物体撕裂的转换都是可以接受的。例如，任何三角形在拓扑上都与其他三角形等价——甚至与圆等价——但与直线不等价。
拓扑不仅在几何中起着至关重要的作用，而且在泛函分析中也起着至关重要的作用。函数通常“生活”在具有无限维度的空间中(例如波函数，它是量子力学的基础)。它对p-adic数也很重要，p-adic数具有奇异的“分形”拓扑结构。
一个大统一2018年左右，Scholze和Clausen开始意识到，拓扑概念的传统方法导致了这三个数学宇宙之间的不兼容性——几何、泛函分析和p-adic数——但另一种基础可以弥补这些差距。这些领域中的许多结果似乎在其他领域中也有相似之处，尽管它们处理的显然是完全不同的概念。但是，一旦拓扑被“正确”地定义，理论之间的类比就会被揭示为相同的“浓缩数学”的实例，这两位研究者提出。克劳森说，这是三个领域的“某种大统一”。
Scholze和Clausen说，他们已经发现了一些更简单、“浓缩”的证明，可以证明许多深奥的几何事实，他们现在可以证明以前未知的定理。他们还没有公开这些信息。
然而，有一个难题:为了证明几何符合这一理论，Scholze和Clausen必须证明一个关于普通实数集的高度技术性定理，该定理具有直线的拓扑结构。“这就像允许实数进入这个新框架的基本定理，”Commelin解释道。
在证明辅助包Lean中，用户可以根据Lean库中已经存在的更简单的语句和概念输入数学语句。在这里Scholze和Clausen的关键结果的输出是一个复杂的网络。这些陈述已经用颜色编码，并按数学的子领域分组。
克劳森回忆起Scholze是如何不屈不挠地进行证明，直到它“通过意志的力量”完成，在这个过程中产生了许多原创的想法。克劳森回忆说:“这是我所见过的最惊人的数学壮举。”但是争论是如此的复杂，以致于Scholze自己担心可能会有一些微妙的差距使整个企业失效。克劳森说:“这看起来很有说服力，但实在是太新颖了。”
为了帮助检查工作，Scholze求助于Buzzard，他是一个数字理论家，也是精益(一个证明辅助软件包)方面的专家。精益最初是由位于华盛顿州雷德蒙德的微软研究院的一位计算机科学家发明的，目的是为了严格检查计算机代码中的错误。
Buzzard一直在运行一个多年的项目，将帝国理工学院的整个本科数学课程编码为精益。他还尝试在这个系统中加入更高级的数学，包括完美空间的概念，这帮助Scholze在2018年获得了菲尔兹奖章。
同样是数字理论家的Commelin带头验证了Scholze和Clausen的证明。Commelin和Scholze决定将他们的精益项目命名为“液体张量实验”(Liquid Tensor Experiment)，以此向前卫摇滚乐队“液体张量实验”(Liquid张量实验)致敬，两位数学家都是该乐队的粉丝。
随之而来的是狂热的在线合作。十几位在精益方面有经验的数学家加入了进来，研究人员在这个过程中得到了计算机科学家的帮助。到6月初，团队已经将Scholze证明的核心——最让他担心的部分——完全转化为精益。这一切都得到了验证，软件能够验证这部分证明。
更好的理解Commelin说，Scholze证明的精益版本包含了数万行代码，比原始版本长了100倍。“如果你只看精益代码，你将很难理解证明，特别是它现在的方式。”但研究人员表示，让证据在计算机上运行的努力也帮助他们更好地理解了它。
AI哥白尼“发现”了地球绕着太阳转
Riehl是尝试使用证明助手的数学家之一，甚至在她的一些本科课程中教授这些助手。她说，虽然她没有系统地在她的研究中使用它们，但它们已经开始改变她对构建数学概念、陈述和证明有关它们的定理的实践的固有思维方式。“以前，我认为证明和构建是两个不同的东西，现在我认为它们是一样的。”
许多研究人员说，数学家不太可能很快被机器取代。巴泽德说，证明助手不能阅读数学课本，他们需要人类不断地输入，他们不能决定一个数学陈述是有趣的还是深刻的——只能决定它是否正确。尽管如此，计算机可能很快就能指出数学家们没有注意到的已知事实的后果，他补充道。
Scholze说，他对证据助手能走多远感到惊讶，但他不确定他们是否会继续在他的研究中发挥主要作用。“现在，我真的不知道它们会对我作为数学家的创造性工作有什么帮助。”