AI人工智能在国际象棋和围棋等问题挑战中击败了人类。下一个会是数学研究吗？Steven Strogatz（量子杂志播客The Joy of Why播主）与数学家 Kevin Buzzard（凯文·巴扎德，英国帝国理工学院纯数学教授）交谈，了解如何将数学翻译成计算机可以理解的语言。
播主：Steven Strogatz 2022-6-29
译者：zzllrr小乐 2022-7-2
译者注：Kevin Buzzard教授也会在今年ICM 2022国际数学家大会中给出1小时大会报告《数学形式主义的兴起》，时间是下周六上午第一场（2022-7-9 10:15）
数学家Kevin Buzzard的自我简介：
我的背景是代数数论，尽管最近我开始在形式证明验证领域工作。我相信计算机将能够在我有生之年帮助人类进行证明，我正在积极尝试通过（a）帮助建立现代数学定理和定义的数据库以及（b）尝试教授数学本科生来早日实现这一目标如何使用该软件。
前言：
如何向AI人工智能教授数学？人工智能已经在一些解题任务上比人类更胜任，包括国际象棋和围棋等游戏。但是，在机器可以处理任何任务之前，必须将其重新解释为计算机可以理解的语言指示。在过去几年里，世界各地的研究人员和业余爱好者共同努力，将数学的基本公理转化为一种称为Lean的编程语言。有了这些知识，了解Lean的定理证明程序已经开始帮助世界上一些最伟大的数学家验证他们的工作。史蒂文·斯特罗加茨（Steven Strogatz）与伦敦帝国理工学院的纯数学教授凯文·巴扎德（Kevin Buzzard），关于给Lean“教”数学的努力——以及像这样的项目如何塑造数学的未来展开交谈。
正文：
Steven Strogatz (00:02)：我是 Steve Strogatz，这是来自量子杂志的播客，带您了解当今科学和数学中一些最大的悬而未决的问题。在这一集中，我们将讨论计算机在数学领域的未来。
(00:19) 计算机能做多少数学运算？计算机能否真正擅长它，甚至比最优秀的人类数学家还要好？如果这听起来有些牵强，那么请记住不久前国际象棋中发生的事情。您可能听说过名为深蓝Deep Blue 的 IBM 计算机，它在 1997 年成功击败了世界上最好的人类棋手Garry Kasparov。当然，作为计算机，Deep Blue 的速度非常快。它每秒可以评估 2 亿个国际象棋位置。它基于其程序员内置的庞大国际象棋知识库对这些位置的评估。
(01:01) 现在，以类似的方式，一个规模虽小但不断壮大的数学家社区一直在忙于用一种名为 Lean 的编程语言编写代码。他们正在建立一个数学知识库，供 Lean 参考，以帮助人类数学家检查他们的证明。凭借代数、几何和逻辑知识，这些被称为证明助手的程序为人们完成繁忙的工作，严格检查他们的工作。这为数学家腾出时间和精神空间，让他们更有创造力。最近，Lean 帮助了世界上最伟大的数学家之一Peter Scholze（彼得·舒尔茨，德国教授，2018菲尔兹奖得主之一，zzllrr译注），验证他正在处理的复杂证明的准确性。这背后有一个有趣的故事，我们会讲到，但这对于这个软件来说是一个巨大的公关胜利。所以问题是，现在和未来几年，计算机能为纯数学做什么？它们会从单纯的证明助手转变为真正的证明创建者吗？如果是这样，像我和我的客人这样的数学家会失业吗？不仅计算会失业，而且思想也失业？所以有请伦敦帝国理工学院纯数学教授 Kevin Buzzard（凯文·巴扎德）。欢迎，凯文。
Kevin Buzzard (02:16)：嗨，谢谢你邀请我。
Strogatz (02:18)：嗯，非常感谢你来到这里。这是一个非常吸引人的话题。我很高兴能和你谈论这件事。那么我们为什么不从Lean是什么开始呢？你能为我们总结一下它是什么吗？首先为什么创建它？
Buzzard (02:32)：我不知道微软为什么首先写Lean，坦率地说，但它知道数学规则，它会仔细倾听你的意见，并识别出任何你说得不精确的东西。它能够以某种有趣的方式学习。它能够检查你所说的话。你可以和它谈论数学，它会理解。这就是我们现在所处的境地。
(03:00) 嗯，现在，它有点像本科生。我把它当作本科生对待。我告诉它本科生的故事。当我不够精确时，它会大惊小怪。但是，它是一个计算机证明检查器。所以我们可以输入数学证明，它来检查通过。最后，如果它相信，那么它会说，“是的，好吧，当然，我明白了。” 但相信意味着什么？在 Lean 的案例中，这意味着它接受了你告诉它的东西，并将这些东西直接转化为数学的基本公理，并检查一切是否正确。
Strogatz (03:38)：我想和你对它探索更多一些。但是——你说你不知道微软为什么要开发它，但也许你至少应该据你所知向我们提供所发生的历史。
Buzzard (03:47)：好的，定理证明器从 1960 年代、1970 年代就已经存在。我不是计算机科学家——但我的印象是，这些东西的设计考虑了两个想法。首先，要验证数学证明是正确的。事实上，早期的定理证明器，你会看到很多证明，比如……2的平方根的无理性。而且，它们的弓还有另一根弦。它们还可以验证计算机代码没有错误。检查软件没有错误听起来像是一个非常强大的应用程序。所以我可以想象，对于像微软这样的公司来说，这是他们想到的事情之一。
(04:35) 然而，我的印象是，在 2014 年这个项目开始时，Leo de Moura设计了一种更简单的解谜器，可以解决逻辑问题——可以非常快速地解决逻辑问题。他为此获奖。他在微软研究院工作，这是微软的天马行空的想象能力（blue-sky thinking wing）。不知何故，他萌生了写一个定理证明器的想法，他很感兴趣，坐下来写了下来。而且我真的不知道他们在想它的去向。但到 2015 年，他们有了原型，到 2017 年，他们有了一些运行良好的东西。
凯文·巴扎德
(05:17) 然后我因为Tom Hales（汤姆·黑尔斯）在剑桥牛顿研究所的一次演讲而遇到了它。汤姆·黑尔斯发表了一场关于数学走向的演讲——一场非常投机的演讲，他认为定理证明器可能是其中的一部分。他提议建立一个数学定理数据库，只是数学定理的陈述，所有这些都在定理证明器中准确而正确地陈述。因为他认为这个数据库可能对数学家有用。所以数据库不会包含所有定理的证明，因为这在某种程度上是不可想象的。追赶将是极其困难的。要知道，数学已经发展了 2000 年。
(06:05) 在最后的问题中，有人问他要使用哪个系统，他说Lean。我从来没有听说过这个软件，但你知道，现在我们有了互联网。所以我搜索了，我搜索了 Lean，发现它相对较新，几乎没有任何数学内容。而且我认为也许值得尝试使用该软件。但是由于几个技术原因，Lean比其他一些定理证明器更有优势，因为你可以写——我的意思是，这有点技术性，但人类不想在公理化的层面上与计算机交谈，对吗？人类宁愿像与人交谈一样与计算机交谈，他们会说，“哦，现在只需将其相乘，然后使用归纳法，然后我们就完成了。” 从那种草图证明到公理，必须有一些东西在后台运行，试图解释正在发生的事情并将其全部转化为数学的基本公理。所以这些东西叫做策略（tactics）。还有一件事，Lean的一个有趣特性是可以用Lean的编程语言编写Lean策略。所以这是一种一体适用（one-size-fits-all）的事情，你可以做数学，你也可以编写算法，将数学转化为公理，所有这些都在同一个系统中。在数学方面，与其他定理证明器相比，这给了 Lean 一点优势。
Strogatz (07:28)：这是一件有趣的事情。所以，你说，策略的想法让那些不一定是计算机科学博士，甚至是计算机类的人，用数学家熟悉的自然语言说话会更舒服. 然而某种程度上，它可以进行翻译。
Buzzard (07:48)：是的，你必须明白公理，对吧？也就是说，这就是游戏规则。归根结底，Lean只是开始了解数学公理，这是非常原始的陈述。事实上，你问大多数数学家，他们无法告诉你数学公理是什么。
Strogatz (08:03)：是的。您能否提醒我们您的意思，或者给我们举一两个例子？
Buzzard (08:08)：嗯，我想，集合论的一个公理是“存在一个集合”。另一个公理是，“如果两个集合具有相同的元素，则它们是相等的。” 再比如“两个集合的并集是一个集合”之类的东西。所以你需要确保，你知道，我们想要检查 ( x + y )，所有的平方，是x²+ 2 xy + y²。我们想扩大括号。如果你尝试从数学公理中执行此操作，则大约需要 20 行。而学校的孩子们都可以告诉你 ( x + y )²是x² + 2xy + y²。我们想要的是——需要一步，不能是 20 步，否则整个事情就会陷入停顿。所以策略是这些更强大的论证，人们可以使用它来让你更像是在与一个聪明的本科生交流，而不是一台除了逻辑中的基本步骤之外什么都不做的死板机器。
Strogatz (09:06)：实际上，我喜欢策略这个词本身，因为策略表明我们正在思考游戏。具体来说，它让我想起了国际象棋。我的意思是，你一直在提到步骤和策略。当然，这些是我们在国际象棋中使用的词。
Buzzard(09:20)：我目前对数学的理解是，数学是一个巨大的益智游戏。事实上，它很快就成为了我最喜欢的益智游戏，真的。我以前在业余时间玩电脑游戏。我喜欢电脑游戏中的谜题。例如，我喜欢塞尔达传说，其中有很多非常诡异的谜题。但也有战斗。还有，你知道的，需要快速的移动和快速的反应时间。随着年龄的增长，我发现故事的这些部分变得不那么有趣了，因为，你知道，我的反应时间变慢了。而且我发现与敌人作战相当乏味。而我发现解决问题非常令人兴奋。而我在 2017 年开始使用 Lean 时发现，实际上，我真的不再玩所有其他电脑游戏了。Lean将数学变成了益智游戏。我的意思是，所有这些定理证明都可以。每个定理证明器都将数学变成了益智游戏。数学定理是那个益智游戏的一个关卡。如果你陈述了这个定理，那么你已经过了这一关。如果你证明了这个定理，那么你就解决了这一关。
Strogatz (10:28)：昨天，我碰巧检查了一个链接，在准备我们今天的讨论时，你有一个排行榜，这也让我想起了游戏。我查看并看到正在创建的数学库中现在有大约 70000 个定理。还有谁在Lean上花费了多少小时的列表。
Buzzard (10:50): 这不是几个小时。这是代码行数，是他们衡量的。
Strogatz：这是代码行数？
Buzzard：是的，我们正在计算代码行数。或者我们也可以统计已证明的定理个数。是的，有排行榜。我不是一个很有竞争力的人。所以我不试图在这些排行榜上名列前茅。但是，这种事情实际上确实很有效。剑桥有个本科生，Yaël Dillies，大约六个月前才对这个软件感兴趣的人。而且我确实注意到，试图在排行榜上获得更高的排名是他非常重视的事情。我真的没有意识到这对某些人来说是一场比赛。我正在采取一些更广泛的观点，我只是希望看到库（library）的成长。你知道，Lean社区是一群令人难以置信的人。数学家和计算机科学家，以我从未见过的方式相互交流和合作。
Strogatz (11:42)：好吧，让我们在这里小心区分，因为我认为，到目前为止，在我们的语言中，我们可能还没有详细说明我们应该详细说明的内容。Lean和库之间的区别。那么，库与Lean有何关系？
Buzzard (11:57)：Lean是一切的动力。但Lean本身对数学几乎一无所知。它知道自然数或整数。它知道一些关于这些东西的基本事实。例如，它知道您可以将整数相加和相乘获得所有整数。也知道您可以将整数相加和相乘一起做。但是诸如实数之类的东西，数轴，大多数数学家，认为理所当然的东西。你不需要这些东西来使核心Lean工作。核心的Lean 只需要可以成为一门编程语言的绝对基础。
(12:32) 那么，数学到哪里去了？好吧，在 2017 年，他们决定诞生这个新的数学库。它被称为mathlib，是 Lean 的数学库（ https://leanprover-community.github.io/mathlib_docs/index.html ）。在当时，你知道，这是一个非常小的项目。当时的想法是，它将是计算机检查的数学，由 Lean 进行检查。所以Lean是一种编程语言。除了作为定理证明器之外，Lean 还是一种编程语言。
(13:00) 现在我们有四分之三的一百万行代码，是用这种与定理相对应的编程语言编写的，但这与Lean本身无关。于是，Lean发展壮大，数学库发展壮大。但这是两个不同的实体。Lean由微软运营，数学库由社区运营。我们只是在制作一个可以与他们的软件配合使用的库。
(13:24) 我现在应该说这些开发人员也不为微软工作。我们创建了他们项目的一个分支。所以微软编写了Lean 3 并坚持下去。它是免费的开源软件，他们把它放在那里。但是现在，他们正在努力开发Lean 4。所以社区接管了Lean 3 的运行。所以主要是计算机科学家，维护Lean 3 代码本身。但数学家往往不会去那里。所有的数学家，都对建立库感兴趣。我猜Lean本身就是动力。它进行所有检查，但库是所有数学的去处。
Strogatz (14:01)：实际上，提到Lean 3 和Lean 4，你让我感到紧张。是否存在向后兼容性的问题？比如，是否有可能在一些新版本中Lean和库不兼容？
Buzzard (14:15)：当然，这就是发生的事情。这是故事中有趣的部分之一，真的。我的意思是，微软推出了Lean 3，他们就像说，“好吧，就是这样。现在，让我们看看能否获得用户群。” 然后，也许出于社会学原因，该用户群突然似乎很快出现了。但它似乎充满了数学家，出于某种原因，他们对编写这个数学库感到非常兴奋。
(14:43) 正如我所说，这些定理证明器已经存在了很长时间。但是，数学家并没有真正推动他们进行研究级别的数学。当这种情况开始发生时，我们开始遇到Lean 3 的问题。微软，你知道，特别是德·莫拉，软件的作者，看着我们正在做的事情——就像在说，“你知道吗，我觉得我想重新开始。以更好的方式从头开始重写整个东西。” 所以微软在过去一年左右一直在编写Lean 4，它并不能向后兼容Lean 3，因为有一些严重的设计变化。所以现在我们有一个巨大的数学库，我们有这个全新的 Lean 4。
(15:37) 所以现在，这在某种程度上是Lean 4 社区中发生的主要事情。他们正在编写一个计算机程序，它将把百万行数学中的四分之三从Lean 3 翻译成Lean 4。他们说，在几个月内，他们可能会完成。但这是一个极其困难的问题。
(15:55) 事实上，我觉得我有部分责任，因为微软找到我并说，“你为什么要推这个数学库？因为我们还没有完全准备好。Lean 3 是一个实验。” 我的回答是，“我真的很抱歉，但我不能停下来，因为这太有趣了。”
Steve Strogatz (16:12)：Lean倚靠的是什么？
Buzzard (16:13)：Lean的倚靠在于它有一个相当小的内核。这是关于信任问题。这更像是计算机科学的事情。这个想法是，说一个定理是正确的，我们的意思是什么？你可能遇到物理学家，他们会说“好吧，只要有足够的数值数据，这是一个完全可靠的、可行的假设，可以用于物理学。” 然后你遇到数学家，他们会说，“嗯，实际上，我们真正想要的是一个证明。我们的意思是，发表在著名数学期刊上的期刊文章，而且，它经历了审稿过程和类似的事情。”
但是计算机科学家很快就指出，实际上，数学文献的语料库中充满了错误，对吧？当我们说一个定理被证明时，有时我们会说，“哦，这个定理是真的。” 但是，五年后，我们不得不回滚这一点，因为一些聪明的研究生在引理 4.3 的证明中发现了一些错误。
(17:12) 或者在数学界偶尔会有一些争论。计算机科学家的意思是“嗯，实际上，我们提供了更好的东西，因为，如果你设法用Lean证明了一个定理，那么它就会被检查确认一直到达数学公理。” 好的，但现在让我们变得更加偏执。如果Lean中有一个错误怎么办，对吧？但是这个想法是Lean的内核应该非常小。因此，如果您真的担心Lean中存在错误，并且您是计算机科学家，那么为什么不继续阅读该代码呢？因为这不是一个不合乎情理的术语。
Strogatz (17:45)：这几乎就像计算机级别的同行评审。
Buzzard (17:48)：是的，这是计算机同行评审。所以一个人真的可以做到这一点。有人可以在不同的操作系统上运行不同的程序，用不同的语言编写，可以进行同行评审。但作为一名数学家，我并不太在意这个。我的意思是，在某种程度上，我认为这有点荒谬。如果我理解证明，或者如果我的社区理解证明，我很高兴地说这是真的。例如，费马大定理，我非常高兴地说，费马大定理已经被数学界证明了，尽管用Lean证明它需要数百人年的工作量。
Strogatz (18:22)：这提出了一个问题——让我们回到这个问题。你提到一些东西已经教给了Lean，一些数学部分，一些分支，我得到了一些印象——嗯，你提到了费马大定理。所有进入其中的巨大数学工具还不是数学库的一部分。那么目前那里有什么东西，以及即将发生的事情？
Buzzard (18:45)：库已经存在四年了。而且我认为有趣的是，它知道的知识与在学校度过了四年的本科生知道的一样多。因此，它的学习速度似乎与人类大致相同。但是，当然，让我强调一下，它的思维方式与人类不同，对吧？它正在检查人类正在输入的结果，对吗？你给它一个问题，它会说，“是的，好的，我理解问题的陈述。” 但是你请一个本科生来解决这个问题，这个本科生可能会着手去想主意。而现在，Lean 只是说，“嗯，我会很高兴——如果你输入一个解，我就能验证那个解是正确的。
Strogatz (19:23)：在我的介绍中，我提到了 Peter Scholze，他是一位数学界的杰出人物，他来找你做Lean的工作。请告诉我们发生了什么。
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 是菲尔兹奖得主，所以也许人们会认为，嗯，他是个聪明人，所以我相信这个定理是正确的。所以他说，“嗯，实际上，也许计算机可以很好地检查这些细节。” 所以，我们认为这将是一个有趣的项目。然后我们慢慢开始了向Lean教学的过程。这个团队也有很多人参与，这是一个协作的努力。任何人都可以加入。有一个剑桥的博士生出现了。滑铁卢的一位研究人员出现了。几个意大利代数几何学家出现了。这些人刚开始出现，就像从woodwork（木工活）里出来，开始做这项工作，将 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)：有人进来，尤其是年轻人，所以出现了更多的项目。我们在Lean社区中实现了指数级增长，数学家们开始感兴趣，参与其中，他们有的在想，“哦，我们为什么不做另一个项目呢？” 例如，我提到费马大定理需要几百人年。所以这仍然是一个非常雄心勃勃的项目。但是对于正则素数（regular primes）证明费马大定理，我的意思是，这是一个已有 100 多年历史的结果。这仍然是一个非常可敬的结果。做这种事情需要相当多的代数数论。
有一群数学家，可能被媒体噪音所吸引，现在正在证明正则素数的费马大定理。还有人在做其他事情，有人在研究球体外翻（sphere eversion）的证明。他们试图证明你可以把球体翻过来。其他项目刚刚出现。而且我认为最终会发生什么，将会发生足够多有趣的事情，最终人们将不得不开始注意到，这个软件正在证明现代数学家正在使用的定理。
Strogatz (24:07)：现在，似乎数学家正在教Lean数学，然后Lean正在做它做得很好的事情，检查逻辑步骤以验证已经概述的证明策略真的可以凑效，所有细节都可以到位，一直到公理级别。但是您是否认为，在某个可能很遥远的未来，Lean的后代将能够自学数学，而不是让人类教师创建库？他们将能够，我不知道，阅读文献，并且有点会自学。
Buzzard (24:48)：我不是计算机科学家。我遇到了很多计算机科学家和人工智能专家，他们绝对专注于这个作为某种主要目标。我遇到过很多乐观主义者，他们会说，所有这一切，都将在 10 年内发生。给我们 10 年，计算机将证明人类无法做到的定理。
(25:14) 我会更加谨慎，因为我知道证明费马大定理需要什么。我的意思是，我是一个代数数论者。而这一切都发生在我读博士生和博士后的时候。费马大定理的证明非常长且技术性很强，为了证明它，我们现在知道的唯一已知证明涉及奇异的、更现代的数学对象，如椭圆曲线（elliptic curve）、模形式（modular form）和伽罗瓦表示（Galois representation）。这些是费马一无所知的东西。这些想法花了很多很多年才形成模形式的概念，结果证明这是完全正确的——它是数论的某种中心概念。
(26:00) 那是数学的艺术部分，对吧？Lean在科学方面做得很好。要知道，一切都是非常严格的定义，有非常非常明确的规则，一个遵循科学，一个证明定理。但是创建模形式的概念或椭圆曲线的概念，或者，伽罗瓦表示的概念，这些都是人类形成的东西。所以，如果计算机不能拥有这些洞察力——而且我还不相信它们能够在所需的水平上拥有这些洞察力——那么在证明我的数学领域的定理时它们将处于很大的劣势，例如，在数论中。
但是，在其他数学分支中，您只是将一些绝妙的想法组合在一起，并且您已经证明了一个新定理，而您根本不需要制造任何新工具。工具已经在那里了。因此，如果我们教计算机，其中一个领域的所有已知工具，然后说，现在继续，开始以十亿不同的方式将它们组合在一起，看看哪些方式是有效的，你可以想象，也许计算机会取得更大的成功。
Strogatz(26:06)：嗯，好吧，这是我希望我们探索的下一个问题的完美设定，即：我们确实在不同的领域中找到了这个问题的答案，在一个比数学——即最高级别的国际象棋领域。我们知道答案是肯定的。因为，我的意思是，深蓝给了我们这个答案。这是一台可以计算国际象棋位置的机器，每秒可以计算 2 亿个位置。它有一个由大师内置的评估功能，用于决定哪些位置是好的，以及哪一方或另一方。它在任何意义上都没有想象力，但它可以计算得非常快。如今，任何人都可以在国际象棋中使用计算机，这基本上会击败地球上的每个人。所以我想我们知道，如果领域足够有限，如国际象棋一样，可以通过纯粹的速度来弥补缺乏想象力。
Buzzard (28:07)：我认为你完全正确。国际象棋是某种有界的领域。但是话又说回来，现在计算机现在可以在围棋上击败人类了，对吧？你也可以说围棋是一个有界领域。但是，你知道，在围棋游戏开始时，你可以下 361 步。因此，当然，五步进入，我们已经得到了，我们得到了非常大的数字。然而，计算机在围棋中击败了人类。此外，他们在没有该数据集的情况下在围棋中击败了人类，对吧？深蓝拥有庞大的数据集，其中包含许多可以使用的大师级国际象棋游戏，但 DeepMind 已经证明，他们可以制造出一台机器，可以通过与自己下棋来真正自学围棋，并且可以很快变得比任何人类都好。
(28:53) 所以棋盘游戏和数学之间的另一个大区别是棋盘游戏是两人游戏。您知道，计算机可以与自己对战，并尝试从自己的错误中学习。它可以犯错误，然后它可以利用错误。数学在某种程度上是一个单人游戏。不是同一种东西。你可以解决一个问题，你可以在一个公理之后抛出一个公理——我们可以在这个问题上一个接着一个地抛出一个定理，并且，发展出越来越多的理论。最后，你有一大堆事实，问题是，你赢了吗？你赢了那场比赛吗？你离证明这个定理更近了吗？现在，我认为这是个大问题。你不知道你是否赢了。
(29:35) 作为一名本科生，我绝对记得这一点。我们试图证明一个定理，讲师在黑板上写下来，我在想，“是的，好吧，所以我们证明了这一点，但是，老实说，这走到哪儿了？我们离证明这个定理更近一步了吗？” 然后突然之间，灵光一闪，然后一切都像下山那样容易。你想出了一个巧妙的想法，就像一个巧妙的举动。然后突然之间变得容易了。这是数学的大问题，你可以关闭你的人工智能，你可以写成百上千行代码。然后你可以退后一步说，“我们真的比开始时更近了吗？还是我们离得更远了？” 现在，我认为这是我们完全不知道的另一个领域。
Strogatz (30:25)：我喜欢你给出的关于成为创造性数学家的计算机的困难表述，因为它让我想起了我们在努力成为创造性的人类数学家时所拥有的很多经验。或者作为导师而言，现在当我有研究生时，我总是看到这一点。学生可以工作多年并想知道，“我们是否更接近获得一个好的博士学位的问题，以及一个好的解？”
Buzzard (30:51)：数学很难。这就是问题。并且以几种不同的方式难。我的意思是，我们现在正在做的一件事是我们正在教计算机科学家数学的难度。我认为在这次合作中发生的一件事是计算机科学家开始更多地了解现代数学的本质。而且，你知道，也许人工智能人员可以从那里拿走它。但这是这次合作的结果之一。
Strogatz (31:22)：这太棒了，凯文。非常感谢您花时间与我们一起探讨这些令人费解的问题。
Buzzard (31:28)：非常感谢。
原文链接：
https://www.quantamagazine.org/can-computers-be-mathematicians-20220629/
转自：arXiv每日学术速递
文章来源于zzllrr小乐 ，作者zzllrr小乐
如有侵权，请联系本站删除！
