计算机可以成为数学家吗？

你如何向人工智能教授数学？人工智能已经在解决问题的任务上击败了人类，包括国际象棋和围棋等游戏。但是，在机器可以处理任何任务之前，必须将其重新解释为计算机可以理解的语言的指示。在过去的几年里，世界各地的研究人员和业余爱好者共同努力，将数学的基本公理转化为一种称为精益的编程语言。有了这些知识，了解精益的定理证明程序已经开始帮助世界上一些最伟大的数学家验证他们的工作。 Steven Strogatz 与伦敦帝国理工学院的纯数学教授Kevin Buzzard讨论了“教”数学到精益的努力——以及像这样的项目如何塑造数学的未来。

在Apple Podcasts 、 Spotify 、 Google Podcasts 、 Stitcher 、 TuneIn或您最喜欢的播客应用程序上收听，或者您可以从Quanta流式传输。

凯文·巴扎德

(05:17) 然后我因为汤姆黑尔斯在剑桥牛顿研究所的一次演讲而遇到了它。汤姆·黑尔斯（Tom Hales）发表了一场关于数学走向的演讲——一场非常投机的演讲，他建议定理证明器可能是其中的一部分。他提议建立一个数学定理数据库，只是数学定理的陈述，所有这些都在定理证明器中准确而正确地陈述。因为他认为这个数据库可能对数学家有用。所以数据库不会包含所有定理的证明，因为这在某种程度上是不可想象的。追赶将是极其困难的。要知道，数学已经发展了 2000 年。

(06:05) 在最后的问题中，有人问他要使用哪个系统，他说精益。我从来没有听说过这个软件，但你知道，现在我们有了互联网。所以我搜索了，我搜索了 Lean，发现它相对较新，几乎没有任何数学内容。而且我认为也许值得尝试使用该软件。但是由于几个技术原因，精益比其他一些定理证明器具有优势，因为你可以写——我的意思是，这有点技术性，但人类不想在公理层面上与计算机交谈，对吧？人类宁愿像与人类交谈一样与计算机交谈，他们会说，“哦，现在只需将其相乘，然后使用归纳法，然后我们就完成了。”为了从这种草图证明到公理，必须有一些东西在后台运行，试图解释正在发生的事情并将其全部转化为数学的基本公理。所以这些东西叫做战术。还有一件事，精益的一个有趣特性是您可以用精益的编程语言编写精益策略。所以这是一种千篇一律的事情，你可以做数学，你也可以编写算法，将数学转化为公理，所有这些都在同一个系统中。在数学方面，与其他定理证明者相比，它给了 Lean 一点优势。

Strogatz (07:28)：这是一件有趣的事情。所以，你说，策略的想法让那些不一定是计算机科学博士，甚至是计算机类的人，用数学家熟悉的自然语言说话会更舒服.然而不知何故，它可以翻译。

Buzzard (07:48)：是的，你必须明白公理，对吧？也就是说，这就是这件事的游戏。归根结底，精益只是开始了解数学公理，这是非常原始的陈述。事实上，你问大多数数学家，他们无法告诉你数学公理是什么。

Strogatz (08:03)：是的。您能否提醒我们您的意思，或者给我们举一两个例子？

Buzzard (08:08)：嗯，我想，集合论的一个公理是“存在一个集合”。另一个公理是，“如果两个集合具有相同的元素，则它们是相等的。”所以这些东西是——或者“两个集合的并集是一个集合”之类的东西。所以你需要确保，你知道，我们想要检查 ( x + y )，所有的平方，是x ² + 2 xy + y ² 。我们想扩大括号。如果您尝试从数学公理中执行此操作，则大约需要 20 行。而任何小学生都可以告诉你 ( x + y ) ²是x ² + 2 xy + y ² 。我们想要——这需要一步，不能是 20 步，否则整个事情就会陷入停顿。所以战术是这些更强大、更强大的论点，人们可以使用它来让你更像是在与聪明的本科生交流，而不是与除了逻辑中的基本步骤什么都不做的死板机器。

Strogatz (09:06)：实际上，我喜欢这个词本身，因为战术表明我们正在考虑游戏。具体来说，它让我想起了国际象棋。我的意思是，你一直在提到动作和战术。当然，这些是我们在国际象棋中使用的词。

Buzzard (09:20)：我目前对数学的理解是，数学是一个巨大的益智游戏。事实上，它很快就成为了我最喜欢的益智游戏，真的。我以前在业余时间玩电脑游戏。我喜欢电脑游戏中的谜题。例如，我喜欢塞尔达系列，其中有很多非常诡异的谜题。但也有战斗。还有，你知道，还有一些事情，你知道，需要快速的移动和快速的反应时间。随着年龄的增长，我发现故事的这些部分变得不那么有趣了，因为我，你知道，我的反应时间变慢了。而且我发现与敌人作战相当乏味。而我发现解决问题非常令人兴奋。而我在 2017 年开始使用 Lean 时发现，实际上，我真的不再玩所有其他电脑游戏了。精益将数学变成了益智游戏。我的意思是，所有这些定理证明都可以。每个定理证明者都将数学变成了益智游戏。数学定理是那个益智游戏的一个层次。如果你陈述了这个定理，那么你已经达到了水平。如果你证明了这个定理，那么你就解决了这个问题。

Strogatz (10:28)：昨天，我碰巧检查了一个链接，在准备我们今天的讨论时，你有一个排行榜，这也让我想起了游戏。我查看并看到正在创建的数学库中现在有大约 70,000 个定理。还有谁在精益上花费了多少小时的列表。

Buzzard (10:50): 这不是几个小时。这是代码行，是他们衡量的。

Strogatz ：这是代码行。

Buzzard ：我们正在计算代码行数，是的。或者我们也可以计算已证明的定理。是的，有排行榜。我不是一个很有竞争力的人。所以我不试图在这些排行榜上名列前茅。但是，这种事情实际上确实很有效。剑桥的一名本科生Yaël Dillies大约在六个月前才对这个软件产生了兴趣。而且我确实注意到，试图在排行榜上获得更高的排名是他非常重视的事情。我真的没有意识到这对某些人来说是一场比赛。我正在采取一些更广泛的观点，你知道，我只是希望看到图书馆成长。你知道，精益社区是一群令人难以置信的人。这是数学家和计算机科学家，你知道，以我从未见过的方式相互交流和合作。

Strogatz (11:42)：好吧，让我们在这里小心区分，因为我认为，到目前为止，在我们的语言中，我们可能还没有详细说明我们应该详细说明的内容。精益和图书馆之间的区别。那么，图书馆与精益有何关系？

Buzzard (11:57)：所以精益是一切的动力。但精益本身对数学几乎一无所知。它知道自然数或整数。它知道一些关于这些事情的基本事实。例如，它知道您可以将整数相加和相乘以获得整数。它知道您可以将整数相加和相乘。但是诸如实数之类的东西，你知道的，数轴，大多数数学家，你知道的，认为理所当然的东西。你不需要这些东西来使核心精益工作。 Core Lean 只需要绝对基础就可以成为一门编程语言。

(12:32) 那么，数学到哪里去了？好吧，在 2017 年，他们决定诞生这个新的数学库。它被称为mathlib ，是 Lean 的数学库。在当时，你知道，这是一个非常小的项目。当时的想法是，它将是计算机检查的数学，由 Lean 进行检查。所以精益是一种编程语言。除了作为定理证明者之外，Lean 还是一种编程语言。

(13:00) 现在我们有四分之三的一百万行代码——你知道，一百万行代码的四分之三，是用这种与定理相对应的编程语言编写的，但这与精益本身无关。于是，精益发展壮大，数学图书馆发展壮大。但这是两个不同的实体。精益由微软运营，数学库由社区运营。你知道，我们只是在制作一个可以与他们的软件配合使用的库。

(13:24) 我现在应该说这些开发人员也不为微软工作。我们创建了他们项目的一个分支。所以微软编写了精益 3 并坚持下去。它是免费的开源软件，他们把它放在那里。但是现在，他们正在努力开发精益 4。所以社区接管了精益 3 的运行。所以主要是计算机科学家，维护精益 3 代码本身。但数学家往往不会去那里。所有的数学家，都对建立图书馆感兴趣。我猜精益本身就是动力。它进行所有检查，但图书馆是所有数学的去处。

Strogatz (14:01)：实际上，提到精益 3 和精益 4，你让我感到紧张。是否存在向后兼容性的问题？比如，是否有可能在一些新版本中进行精益，而你和库不兼容？

Buzzard (14:15)：当然，这就是发生的事情。这是故事中有趣的部分之一，真的。我的意思是，微软推出了精益 3，他们就像，“好吧，就是这样。现在，让我们看看能否获得用户群。”然后，也许出于社会学原因，该用户群突然似乎很快出现了。但它似乎充满了数学家，出于某种原因，他们对编写这个数学库感到非常兴奋。

(14:43) 正如我所说，这些定理证明器已经存在了很长时间。但是，数学家并没有真正推动他们进行研究级数学。当这种情况开始发生时，我们开始遇到精益 3 的问题。微软，你知道，特别是德莫拉，你知道，软件的作者，看着我们正在做的事情——就像，“你知道吗，我觉得我想重新开始。你知道，以更好的方式从头开始重写整个事情。”所以微软在过去一年左右一直在编写精益 4，它并不能向后兼容精益 3，因为有一些严重的设计变化。所以现在我们有一个巨大的数学库，我们有这个全新的 Lean 4。还有一个很大的问题是“我们如何将这个数学库纳入 Lean 4？”

(15:37) 所以现在，这在某种程度上是精益 4 社区中发生的主要事情。他们正在编写一个计算机程序，它将把百万行数学中的四分之三从精益 3 翻译成精益 4。他们说，在几个月内，他们可能会完成。但这是一个极其困难的问题。

(15:55) 事实上，我觉得有部分责任，因为微软找到我并说，“你为什么要推这个数学库？因为我们还没有完全准备好。你知道，精益 3 是一个实验。”我的回答是，“我真的很抱歉，但我不能停下来，因为这太有趣了。”

Steve Strogatz (16:12)：精益是什么？

Buzzard (16:13)：精益的精益在于它有一个相当小的内核。这是关于信任问题。这更像是计算机科学的事情。这个想法是，说一个定理是正确的，我们的意思是什么？你可能有物理学家，他们会说“好吧，只要有足够的数值数据，这是一个完全可行的、可行的假设，可以用于物理学。”然后你有数学家，他们会说，“嗯，你知道，实际上，我们真正想要的是一个证明。我们的意思是，你知道，发表在著名数学期刊上的期刊文章，而且，你知道，它经历了审稿过程和类似的事情。”

但是计算机科学家很快就指出，实际上，数学文献的语料库中充满了错误，对吧？当我们说一个定理被证明时，有时我们会说，“哦，这个定理是真的。”但是，五年后，我们不得不回滚这一点，因为一些聪明的研究生在引理 4.3 的证明中发现了一些错误。

(17:12) 或者在数学界偶尔会有一些争论。计算机科学家的意思是“嗯，实际上，我们提供了更好的东西，因为，你知道，如果你设法证明了精益定理，那么它就会被检查到数学公理。”好的，但现在让我们变得更加偏执。如果精益中有一个错误怎么办，对吧？但是这个想法是精益的内核应该非常小。因此，如果您真的担心精益中存在错误，并且您是计算机科学家，那么为什么不继续阅读该代码呢？因为这不是一个不合理的术语。

Strogatz (17:45)：这几乎就像计算机级别的同行评审。

Buzzard (17:48)：是的，这是计算机同行评审。所以一个人真的可以做到这一点。是的，有人可以在不同的操作系统上运行不同的程序，用不同的语言编写，可以进行同行评审。但是——但作为一名数学家，我并不太在意这个。我的意思是，在某种程度上，我认为这有点荒谬。如果我理解证明，或者如果我的社区理解证明，我很高兴地说这是真的。例如，费马大定理，我非常高兴地说，你知道， 费马大定理已经被数学界证明了，尽管用精益证明它需要数百人年的工作量。

Strogatz (18:22)：这提出了一个问题——让我们回到这个问题。你提到一些东西已经教给了精益，一些数学部分，一些分支，我得到了一些印象——嗯，你提到了费马大定理。所有进入其中的巨大数学工具还不是数学库的一部分。那么目前那里有什么东西，以及即将发生的事情？

Buzzard (18:45)：图书馆已经存在四年了。而且我认为有趣的是，它知道的知识与本科生知道的一样多，如果他们在学校度过了四年。因此，它的学习速度似乎与人类大致相同。但是，当然，让我强调一下，它的思维方式与人类不同，对吧？它正在检查人类正在输入的结果，对吗？你给它一个问题，它会说，“是的，好的，我理解问题的陈述。”但是你请一个本科生来解决这个问题，这个本科生可能会开始有想法。而现在，Lean 只是说，“嗯，你知道，我会很高兴——如果你输入一个解决方案，我就能验证那个解决方案是正确的。

Strogatz (19:23)：在我的介绍中，我提到了 Peter Scholze，他是一位数学界的杰出人物，他来找你做精益的工作。请告诉我们发生了什么。

Buzzard (19:31)：所以，这又回到了证明定理意味着什么的想法。我们怎么知道，我们怎么知道一个定理是正确的，对吧？因此，Peter Scholze 和Dustin Clausen正在开发一种新理论，他们希望他们的新理论能够使代数技术能够用于特定的分析分支。这会很酷，因为突然之间，会有一大堆新技术可以用来解决以前很难解决的问题。所以 Scholze 和 Clausen 提出了一些想法，我猜 Scholze 在 2019 年和 2020 年在波恩就这些想法做了一些讲座。讲义已经在互联网上发布。在这些讲义中，有一些定理，你知道，它们以某种方式将整个事情结合在一起。

(20:21) 这是 Scholze 决定做的实验。他想，“嗯，你知道，这些东西已经存在了一段时间。我不知道现在有哪些数学家仔细检查过它？”但他对第二门课程中的一个特定定理特别感兴趣，即定理 9.1。所以他联系了我说：“你知道，你在帝国理工读过这些报纸吗？我说，“是的，我们会，你知道，我们花了很多时间来查看它们。”然后他说：“那么你检查定理 9.1 的所有细节了吗？”我说，“不，我们没有。我们有两个小时到达第 9 章。我们必须对它进行一些概述。所以我们没有检查所有的技术细节。”所以他提出了一个问题，谁来检查定理 9.1 的这些技术细节？

(21:07) 也许没有人会阅读证明。但是，当然，你知道，Scholze 是菲尔兹奖得主，所以也许人们会认为，嗯，你知道，他是个聪明人，所以我相信这个定理是正确的。所以他说，“嗯，实际上，也许计算机可以很好地检查这些细节。”所以，我们认为这将是一个有趣的项目。然后我们慢慢开始了向精益教学的过程。这个团队，我的意思是，也有很多人参与，这是一个协作的努力。任何人都可以加入。有——一个博士。剑桥的学生出现了。你知道，滑铁卢的一位研究人员出现了。几个意大利代数几何学家出现了。这些人刚开始出现，刚从木制品里出来，开始做这项工作，将数学中的 Scholze-Clausen 单词翻译成 Lean 的语言，因为这真的是某种翻译过程。

(21:59) 所以这个翻译过程花了大约五个月的时间。到那时，我们已经证明了定理 9.4。我们目前——我们还没有完成，因为我们还没有翻译定理 9.4 蕴含定理 9.1 的证明。但事实证明，我们并没有意识到这一点，但是当我们完成定理 9.4 时，Scholze 说，“好吧，现在我相信了。”这显然是他担心的事情。 9.4 到 9.1 有点概念化，他对这个论点很有信心。 9.4 的证明是他担心我们目前的系统永远不会检查细节的事情，所以现在一台计算机已经检查了它。所以他基本上宣布，现在，他很高兴。

Strogatz (22:43)：好吧，让我问一下你提出的社会学问题。你说你会认为，鉴于定理 9.4 证明的成功，更保守的反对者现在会开始加入。是这样吗？据你所知？

Buzzard (22:58)：有人进来，尤其是年轻人，所以出现了更多的项目。我们在精益社区中实现了指数级增长，数学家们开始感兴趣，参与其中，他们有点想，“哦，我们为什么不做另一个项目呢？”你知道，例如，我提到费马大定理真的，你知道，几百人年。所以这仍然是一个非常雄心勃勃的项目。但是证明费马大定理对于常规素数，我的意思是，这是一个已有 100 多年历史的结果。这仍然是，这仍然是一个非常可敬的结果。你知道，做这种事情需要相当多的代数数论。

我有一群数学家，我们可能被媒体噪音所吸引，现在正在证明正则素数的费马大定理。还有人在做其他事情，有人在研究球体外翻的证明。他们试图证明你可以把球体翻过来。其他项目刚刚出现。而且我认为最终会发生什么，将会发生足够多有趣的事情，最终人们将不得不开始注意到，这个软件正在证明现代数学家正在使用的定理。

Strogatz (24:07)：所以现在，似乎数学家正在向 Lean 教授数学，然后 Lean 正在做它做得很好的事情，检查逻辑步骤以验证已经概述的证明策略真的可以制定工作，所有细节都可以到位，一直到公理级别。但是您是否认为，在某个可能很遥远的未来，精益的后代将能够自学数学，而不是让人类教师创建图书馆？他们将能够，我不知道，阅读文献，并且有点自学。

Buzzard (24:48)：所以我不是计算机科学家。我遇到了很多计算机科学家和人工智能专家，他们绝对专注于这个作为某种主要目标。我遇到过很多乐观主义者，他们会说，所有这一切，你知道，这一切都将在 10 年内发生。给我们 10 年，计算机将证明人类无法做到的定理。

(25:14) 我会更加谨慎，因为我知道证明费马大定理需要什么。我的意思是，我是一个代数数论者。而这一切都发生在我攻读博士学位的时候。学生和博士后。费马大定理的证明非常冗长且技术性很强，为了证明它，我们现在知道的唯一已知证明涉及奇异的、更现代的数学对象，如椭圆曲线、模形式和伽罗瓦表示。这些是，这些是费马一无所知的事情。这些想法花了很多很多年才形成模形式的概念，结果证明这是完全正确的——它是数论的某种中心概念。

(26:00) 你知道，那是数学的艺术部分，对吧？你知道，精益在科学方面做得很好。要知道，一切都是非常严格的定义，有非常非常明确的规则，一个遵循科学，一个证明定理。但是创建模形式的概念或椭圆曲线的概念，或者，你知道， 伽罗瓦表示的概念，这些都是人类形成的东西。所以，如果计算机不能拥有这些洞察力——而且我还不相信它们能够在所需的水平上拥有这些洞察力——那么在证明我的数学领域的定理时它们将处于很大的劣势，例如，在数论中。

但是，在其他数学分支中，您只是将一些绝妙的想法组合在一起，并且您已经证明了一个新定理而您没有，您根本不需要制造任何新工具。工具已经在那里了。因此，如果我们教计算机，其中一个领域的所有已知工具，然后说，现在继续，现在开始以十亿不同的方式将它们组合在一起，看看哪些方式是有效的，你可以想象，也许计算机会取得更大的成功。

Strogatz (26:06)：嗯，好吧，这是我希望我们探索的下一个问题的完美设置，即：我们确实在不同的领域，在一个更加受限的领域中找到了这个问题的答案比数学——即最高级别的国际象棋领域。我们知道答案是肯定的。因为，我的意思是，深蓝给了我们这个答案。这是一台可以计算国际象棋位置的机器，每秒可以计算 2 亿个位置。它有一个评估功能，用于决定哪些位置是好的，以及哪一方或另一方，由大师内置。它在任何意义上都没有想象力，但它可以计算得非常快。如今，任何人都可以在国际象棋中使用计算机，这将基本上击败地球上的每个人。所以我想我们知道，是的，如果域足够有限，你可以通过纯粹的速度来弥补缺乏想象力。象棋一样。

Buzzard (28:07)：我认为你完全正确。国际象棋是某种有界域。但是话又说回来，现在计算机现在可以在围棋上击败人类了，对吧？你也可以说 Go 是一个有界域。但是，你知道，在围棋游戏开始时，你可以下 361 步。因此，当然，五步进入，我们已经得到了，你知道，我们得到了非常大的数字。然而，计算机在围棋中击败了人类。此外，他们在没有该数据集的情况下在围棋中击败了人类，对吧？ Deep Blue 拥有庞大的数据集，其中包含许多可以使用的大师级国际象棋游戏，但 DeepMind 已经证明，他们可以制造出一台机器，可以通过与自己下棋来真正自学围棋，并且可以很快变得比任何人类都好。

(28:53) 所以棋盘游戏和数学之间的另一个大区别是棋盘游戏是两人游戏。您知道，计算机可以与自己对战，并尝试从自己的错误中学习。它可以犯错误，然后它可以利用错误。数学在某种程度上是一个单人游戏。不是，不是同一种东西。你可以解决一个问题，你可以在一个公理之后抛出一个公理——我们可以在这个问题上一个接着一个地抛出一个定理，并且，你知道，发展出越来越多的理论。最后，你有一大堆事实，问题是，你赢了吗？你赢了那场比赛吗？你，你——离证明这个定理更近了吗？现在，我认为这是个大问题。你不知道你是否赢了。

(29:35) 作为一名本科生，我绝对记得这一点。我们试图证明一个定理，讲师在黑板上写下来，我在想，“是的，好吧，所以我们证明了这一点，我们证明了这一点，但是，你知道，老实说，这在哪里去？我们离证明这个定理更近一步了吗？”然后突然之间，有一个辉煌的繁荣，然后一切都在走下坡路。你知道，你想出了一个巧妙的想法，就像一个巧妙的举动。然后突然之间变得容易了。这是数学的大问题，你可以，你可以关闭你的人工智能，你可以写成百上千行代码。然后你可以退后一步说，“我们真的比开始时更近了吗？还是我们离得更远了？”现在，我认为这是我们完全不知道的另一个领域。我认为计算机无法解决这个问题。

Strogatz (30:25)：我喜欢你给出的关于成为计算机创造性数学家的困难的表述，因为它让我想起了我们所有人在努力成为人类时所拥有的很多经验创造性的数学家。或者作为顾问，现在，当我有研究生时，我总是看到这一点。学生可以工作多年并想知道，“我们是否更接近获得一个好的博士学位？问题，以及一个好的解决方案？”

Buzzard (30:51)：数学很难。这就是问题。并且以几种不同的方式很难。我的意思是，我们现在正在做的一件事是我们正在教计算机科学家数学的难度。我认为在这次合作中发生的一件事是计算机科学家开始更多地了解现代数学的本质。而且，你知道，也许人工智能人员可以从那里拿走它。但这是这次合作的结果之一。

Strogatz (31:22)：这太棒了，凯文。非常感谢您花时间与我们一起探讨这些令人费解的问题。

Buzzard (31:28)：非常感谢。

播音员(31:31)：如果您喜欢The Joy of Why ，请查看由我主持的Quanta 杂志科学播客，Susan Valot 是该节目的制作人之一。另外，请告诉您的朋友有关此播客的信息，并在您收听的地方给我们点赞或关注。它可以帮助人们找到The Joy of Why播客。

Strogatz (31:51): The Joy of Why是来自Quanta Magazine的播客，这是一份由 Simons Foundation 支持的独立编辑出版物。西蒙斯基金会的资助决定对本播客或Quanta 杂志中的主题、嘉宾或其他编辑决定没有影响。 The Joy of Why由 Susan Valot 和 Polly Stryker 制作。我们的编辑是 John Rennie 和 Thomas Lin。我们的主题音乐由 Richie Johnson 创作，我是您的主持人 Steve Strogatz。如果您对我们有任何问题或意见，我们很乐意听取他们的意见。请发送电子邮件至 [email protected]。谢谢收听。