陶哲轩：AI时代，数学研究将进入前所未有的规模

来源：量子位

编辑：西风

陶哲轩最新演讲公开，AI含量爆表。

在IMO 2024现场，“陶神”带来了洋洋洒洒1个小时的精彩分享，主题就叫：AI与数学。

他怎么看AI和数学的关系？怎么理解机器学习、大模型等在数学领域的应用与发展？

所有观察和观点都毫无保留分享：

借助AI，可以想象未来可以取一类1000个问题同时处理，你真的可以开始以一种前所未有的规模进行数学研究。

除此之外，“陶神”还由古至今讲述了机器辅助计算的传统与演变。

AI等一系列机器在数学研究中的妙用并非空口无凭：

• 毕达哥拉斯三元数组的问题只能使用计算机解决

• 开普勒猜想最终也是借由计算机辅助证明

• 机器学习在纽结理论中的应用：已经能够帮助猜测两种不同统计数据之间的联系

他本人还透露，自己用GPT-4找解题灵感；用GitHub Copilot辅助证明，大概有20%概率，它能写出接近正确的下一步证明。

不光是在演讲中讲AI，陶哲轩最近发布的几个帖子也都和AI息息相关。

网友纷纷安利：

他没有支持或反对AI炒作，而只是理性开放地评估了这些工具及其能力，还有未来可能发生的事。

量子位在不改变原意的基础上，对“陶神”这次最新的演讲内容进行了编译整理。

“陶神”从机器辅助计算的传统开始讲起，又接着讲了大致以下几个板块的内容：

• 计算机起初最基本的用途

• 机器在科学计算中的应用

• 现代用机器进行数学研究的创造性方法：证明助手、机器学习、大语言模型

另外，文末有添加AI字幕的视频版，童鞋们也可以直接拉到最后观看视频～

长期以来就有机器辅助计算的传统

你们都听说过AI以及它如何改变一切。早些时候有一个DeepMind发布了一个AlphaGeometry，现在可以回答一些IMO几何问题。

我将更多地讨论这些工具是如何开始改变数学研究的。

这与数学竞赛不同，不是设定三个小时什么的来解决一个问题，而是需要几个月甚至更长时间，有时解决不了问题，那就必须改变问题。这绝对不同于数学竞赛，尽管在技能上有些重叠。

这一切都非常令人兴奋，它正在开始具有变革性。但另一方面，也有一种连续性的感觉，我们实际上已经使用计算机和机器来做数学运算很长时间了，而我们进行这些运算的方式的本质正在发生变化。

但实际上，这是遵循了长期以来机器辅助的传统。

那么，问题来了。我们使用机器来做数学已经有多久了？答案是数千年。

这是罗马人曾经用来做数学的机器，算盘是早期的机器，甚至还有一些更早的。听起来可能有点无聊，这些并不是非常智能的机器。

计算机呢？我们使用计算机做数学多久了？大约是三四百年。这有点奇怪，因为你知道，我们的电子计算机直到20世纪三四十年代才出现。

但在电子计算机之前，计算机曾经是机械式的，计算机也曾指进行计算的人，是一种职业。

曾经有人力“计算机集群”，人使用加法机计算弹道学等问题，计算能力的基本单位不靠CPU，而是kilgirl，即1000名女性1小时可以完成多少计算任务，当时男人们都在打仗。

计算机最基本的用途是制作表格

人们很早就在使用计算机，正如我之前所说，实际上早在17世纪甚至更早之前就开始使用了。

那时计算机最基本的用途是制作表格（table），你可能听说过纳皮尔的对数表。

如果你想计算正弦、余弦等，你会使用计算机生成这些表格。我高中上课时仍会学习如何使用这些表格，它们刚刚被淘汰。

当然，现在我们有计算器和现代计算机。

我的意思是，在数学研究中，我们依赖于表格，现在我们称它们为数据库，但它们本质上还是一样的东西。

在数学中有许多重要的成果最初是通过表格发现的。

例如，数论中最基本的成果之一——素数定理。它大致告诉你在一个大数x之前有多少个素数，这一发现归功于勒让德和高斯等人。

当时他们虽未能证明它，但由于高斯和其他人使用了早期的计算设备，他们推测这一理论是正确的。实际上，高斯自己就像一个计算机一样，计算表格并尝试找出规律。

之后还出现了另一个重要猜想——Birch and Swinnerton-Dyer猜想，这里不详述。这个猜想也是人类通过查看大量关于曲线的数据表格然后首次发现的。

如今，包括我在内的许多数学家使用的一个表格，是所谓的Online Encyclopedia of Integer Sequences（OEIS），它收集了大量数学序列数据。

也许你遇到过它，像“1, 1, 2, 3, 5, 8,13”，你知道这是斐波那契数列，OEIS是一个数据库，有成千上万这样的序列。

在数学研究中，数学家经常会遇到一些自然出现的数字序列，这些序列可能依赖于变量n，如空间的维数、集合的基数等。

你可以计算这些序列的前五个、六个或十个数字，然后将其输入到OEIS中进行比较。如果幸运的话，这个序列可能已经被别人放在那里了，可能来源于对某个完全不同的数学问题的研究。

这样的发现可以大大提示两个问题之间可能存在的联系，许多研究就是这样开始的。

机器在科学计算中的应用

机器在数学领域的另一个重要应用是科学计算（scientific computation）。

当你需要执行大规模计算时，你会将大量的算术运算任务丢给计算机。自1920年代以来，这一做法已广泛被采用。

也许第一个真正进行科学计算的人是亨德里克·洛伦兹。

我记得是荷兰人想要建一个巨大的堤坝，委托他想弄清楚水流会怎样变化。所以他们必须建立模型和一些流体方程，洛伦兹实际上使用了一群人类“计算机”来解决这个问题，采用了浮点运算。

他意识到，如果你想让很多人很快地完成大量计算，你应该用浮点数来表示各种不同大小的数字。当然，我们现在使用计算机来模拟各种事物。

如果你在解决许多线性方程或者不同的方程，你可能想进行一些组合计算，也可以解决代数问题。你在IMO中看到的许多几何问题原则上都可以通过科学计算来解决。

有一些代数软件包，你可以将任何几何问题，比如涉及10个点和一些线和圆的问题，转化为一个包含20个实数和20个未知数的方程系统，然后输入到如Sage或Maple等软件中。

不过，随着问题规模的扩大，解决问题的计算复杂性可能会呈指数级或双指数级增长，会超出传统计算机代数软件包的处理能力。

因此直到最近，还不可能仅用标准的计算机代数软件包来暴力解决这些问题。但现在有了AI的辅助，情况可能有希望改变。

另一种强大的科学计算类型是所谓的SAT求解器，可以用来解决某种逻辑谜题。

例如，你有1000个或真或假的陈述，而且你知道如果第三个陈述是真的，第六个陈述也是真的，那么第七个陈述必然是假的。如果你给出了一系列这样的约束条件，SAT求解器就会尝试利用所有这些信息，来得出例如能否证明这些陈述中的某些是对还是错等结论。

还有一个更高级的版本称为SMT求解器。如果你有一些变量x、y、z，并且假设一些定律等等，你可以将这些定律和一些其它事实输入进去，尝试简单暴力地在有限的假设中得出结论。

这些非常强大，但也不能很好地扩展。再次强调，问题的复杂度可能使运算时间呈指数增长，因此一旦超过大约1000个命题，对这些求解器来说，再运行就变得非常非常困难。

不过，计算机实际上可以解决一些问题。

例如，一个成功案例是在组合数学中的应用，我认为人类在没有帮助的情况下解决这个问题是不可能的，也许只能通过计算机解决。

问题关于毕达哥拉斯三元组（勾股数组）：

将自然数涂成红色或蓝色两种颜色，无论怎样涂色，是否总有一种颜色包含毕达哥拉斯三元组abc？

此问题以前并未得到验证，直到一台大型计算机进行计算之后才被解决。

现在我们知道，你无需检查所有自然数。

对于自然数1到7824，可以将其分为两种颜色，其中任何一种颜色中都不包含毕达哥拉斯三元组。但对于自然数1到7825，是一定会包含的。

我认为这是当时世界上最长的证明，现在是第二长的证明了。这个证明需要4个CPU年的计算时间，并且最终生成了一个包含200TB数据的证明文件，该文件后来被压缩至86GB。

所以这是使用计算机的一种相当明显的方式。

现在使用计算机研究的三种创意方式

最近几年，我们开始用更具创造性的方式使用计算机，特别是将它们与彼此以及更传统的数据库、表格、科学计算相结合。

我们使用机器学习神经网络以不同于人的方式来发现新的联系，找出不同类型的数学之间的相关方式。

最引人注目的是大语言模型，它可以进行自然语言对话，像ChatGPT、Claude等，有时它们可以产生解决问题的有效方法。

还有另一种技术被数学家们使用——形式证明助手（formal proof assistants）。

这些工具本质上是编程语言，就像你使用计算机语言编写可执行代码一样，形式证明助手是用来检验事物的语言，它们帮助你验证某个论证是否真实，并从数据中得出结论。

最近这些工具的使用变得相对易用，且正在助力许多有趣的数学项目，这些项目在没有形式证明助手的帮助下是不可能实现的。

未来，它们将与我提到的其它工具很好地结合起来。

所以我想谈谈使用现代计算机和机器进行数学研究的方法，从证明助手开始。

1.证明助手

第一个真正的计算机辅助证明也许是四色定理的证明。

这个定理在1976年得到了证明：任何一张地图只用四种颜色进行着色，就能使相邻区域的颜色不相同。

来源｜维基百科

他们证明四色定理的方式基本上是对国家数量进行归纳。你需要展示如果你有一张庞大的地图，那么就会存在一些国家的子图，他们列出了大约1000到2000个特殊的子图，每一个庞大的国家图在某种意义上都必须包含这些子图中的至少一个，这是他们必须检查的一件事。

然后他们必须检查每当你有一个子图时，你可以用更简单的东西替换这个子图，如果你能用四种颜色来着色这个更简单的东西，你就能给主图着色。

还有可简化性，对于这些子图中的每一个都要进行检查。

这些任务中的一些可以由计算机完成，还有一些任务是人工花费数小时手动检查的。

我认为，这是一个需要重新审视的过程，它非常乏味，并且过程并不完美，存在许多小错误。按照现代的计算机证明标准，这并不是一个可以被计算机验证的证明。

这种情况直到90年代才有所改变，那时出现了一个使用大约700个子图的更简单的证明。

2005年，使用Coq证明辅助工具，实现了完全形式化的计算机可验证证明。

我们可以看到，从首次证明出现到我们实际上能够完全通过计算机验证之间有一个巨大的差距。

另一个著名的例子是关于球体最密堆积的几何问题——开普勒猜想。

开普勒猜想称，在三维空间中，最密的球体排列方式是面心立方堆积（FCC）和六方最密堆积（HCP）。这两种排列方式的球体占据的体积比约为74.048%，这是所有可能的排列方式中最大的。

来源｜维基百科

怎么确定这种堆积方式是否是最好的？这成为一个特别难的问题，并没有一个完全对人类可读的猜想证明。

问题在于，对于无穷多的球体，密度是一个渐进的事情，所以它不是一个先验的有限问题，你不能仅仅把它扔给计算机来解决。

但是你可以试着把它简化为有限的问题。

每次进行堆积时，它会将空间细分为被称为Voronoi区域的多面体。球的Voronoi多面体就是所有距离该球中心最近的点所组成的区域，这些多面体都有特定的体积，你还可以计算它们的面数和表面积等，并因此获得这些统计数据。

Toth在20世纪50年代提出了一种策略。他观察到某些加权不等式基于有限多个Voronoi多面体的体积能得到球堆积密度的上界。

你可以尝试建立这些多面体之间的关系，比如，如果一个多面体非常大，可能会迫使附近的多面体变得非常小，因此你可以尝试找到一些连接一个多面体的体积与另一个多面体的体积的不等式。

许多研究者尝试过这种方法，有些甚至声称成功，但没有一个得到认可能作为确切的证明。

最终，这个问题由Thomas Hales及其合作者解决。他采用了基本相同的策略，但加入了许多技术性调整。

他们把Voronoi单元改进得更精细，并不只是简单测量体积，而是创造了一个综合得分，将体积和多个小的临时调整结合起来。他的目标是在这些不同得分之间建立线性不等式，从而最终得到密度的上限，并希望精确地达到最优密度。

这种方法极具灵活性，但也因为可尝试的方案过多而显得过于复杂。

Thomas Hales和其学生Samuel Ferguson意识到，每次他们在解决最小化问题时遇到困难，都能调整评分函数来回避这些困难。函数变得更加复杂，每次更改都可能花费很长时间。

更糟糕的是，这个函数与之前论文中的内容略有不兼容，就需要回头去修改之前的论文。

最初，他们并没有计划依赖计算机，但随着项目变得越来越复杂，必须越来越多地依赖计算机处理。

到1998年，他们最终宣布该项目成功，从一个精心选择的包含150个变量的优化问题中，通过线性规划计算得出了开普勒猜想的证明。

证明包括了250页的笔记和3GB的计算机程序、数据和结果。

这个证明在审核过程中遇到了重大困难。它被提交给了一些顶尖的数学期刊，评审过程耗时四年，由一个专家小组负责。

在评审结束时，他们表示对证明的正确性有99%的把握，但他们无法确认计算机计算的正确性。他们采取了一种非常不寻常的做法，即在发表论文时添加了一个注释来说明这一点。后来，他们撤销了这个注释。

当时，是否接受计算机辅助证明作为正式证明存在很大争议。现在，我们对此更加自信，但即便在论文发表后，关于其是否真正构成证明仍有疑问。

因此，这可能是第一个真正需要将问题完全按照基本原则形式化的高知名度案例。为此，Hales开发了一种语言，称之为Flyspeck项目。

他最初估计需要20年来形式化他们的证明，但实际上，在21位合作者的帮助下，他仅用了12年时间就完成了。最终，这一成果在2014年公布。

因此，我们现在对这一结果充满信心。

我们已经开始探索更好的工作流程来进行形式化，虽然这一过程仍然很繁琐，但正在逐步改进。

Peter Scholze是一位非常杰出的年轻数学家，他因许多成就而闻名，尤其是创建了一个被称为“浓缩数学”的数学领域。

这个领域利用代数、范畴论及其它代数工具，来解决传统上抵抗代数方法的泛函分析和函数空间理论等问题。

Scholze建立了包括所谓的浓缩abelian群和向量空间的一整套范畴。他的主要观点是，我们在研究生课程中学习的所有关于函数空间的分类都是不准确的，或者它们不是最自然的，而他提出的分类具有更好的属性。

然而，有一个非常重要的消失定理他需要证明。这个定理的证明涉及到某个范畴理论群的非常技术性的计算。因此，这成为了他理论的基础。

他在一篇博客文章中讨论了这一结果，提到他花了一整年时间沉迷于这个定理的证明，几乎陷入疯狂。最终，他们设法将论证印刷在纸上，但没有人敢深入探查这些细节，所以他仍然有持续的疑虑。

有了这个定理，这种浓缩公式在泛函分析中的应用才站得住脚。这极为基础且重要，因此，99.9%的确定性还不够。

世界各地有许多关于浓缩数学的研究小组，但他们都未能完成这个定理的证明。这个证明过程并不有趣，所以他说这可能是他最重要的成就，但必须确保其正确性。

后来，使用了一种更现代的、称为Lean的程序语言。

Lean是近些年发展起来的一种语言，它是一个众包项目，旨在开发庞大的数学库。与其从数学的基本公理推导一切，这个库已经证明了许多中间结果，如本科数学课程中可能会看到的基础群论、拓扑学等主题，这些已经被形式化了。

但为了形式化这个理论，他们不得不添加许多额外内容，尽管数学库还不完整，仍有很多领域，如同调代数、层理论等需要添加到库中，但在短短18个月内，他们形式化了这个定理。

证明基本正确，尽管存在一些小的技术问题，但没有发现重大错误，他们找到了一些简化的技巧，有些技术步骤过于复杂而难以形式化，因此他们被迫寻找了一些捷径。

实际上，这个项目的价值更多的是间接的。

首先，他们大大丰富了Lean数学库。现在，这个数学库可以处理大量的抽象代数，远远超过了以前的能力。此外，还有其它支持软件被建立起来，例如blueprint（蓝图）。

直接形式化一个庞大的证明，比如50页的证明，真的很痛苦，你必须把整个证明记在脑海中。

正确的工作流程是，你拿一个大的证明，首先编写一个blueprint，它将这个证明分解成数百个小步骤。每一步都可以单独形式化，然后再将它们全部组合起来。你的团队中不同的人可以在不同的步骤中形式化论证不同部分。

这个项目的另一个成果是，现在我们有了一个由数万行代码组成的形式化证明。目前正在努力将这个证明转换为人类可读的格式。此外，还开发了一些工具，可以将用Lean这种语言编写的证明转换回人类可读的形式。

例如，这里有一个拓扑问题的证明，它已被成功转换为人类可以理解的格式。

因此，这些文本都是从形式化证明中计算机生成的。它看起来像是人类编写的证明，使用了相同类型的数学语言，但更具交互性。

你可以点击任何位置，系统会告诉你当前的假设、你正在尝试证明什么、变量是什么。如果某个步骤太简短，你可以展开它以了解其来源，并且可以深入到你想要的公理。

我认为这是非常好的创新，我相信未来我们编写的教科书将采用这种互动式风格，首先进行形式化，然后你将拥有比现有教科书更具互动性的版本。

受此启发，我自己也开始了一个形式化的项目。

去年，我与包括Tim Gowers在内的几个人一起解决了一个组合学问题。它涉及到一个具有“小倍增”性质的二进制Hamming立方体的子集，这个子集的大小有一定的限制。

我们在相对较短的时间内将其形式化，证明大约有33页长。

实际上，这可能仍是迄今为止最快完成形式化的实际研究论文，在三周内由大约20人的团队完成，利用了Scholze项目中开发的所有这些blueprint。

因此，它使得证明任务变得更加开放，协作性更强，你还可以获得精美的可视化效果。

正如我所说，你要做的第一件事是把你的大定理分解成许多小块。我们得到的定理称为PFR，对应于这里图表底部的一个小圈。

然后我们引入了所有这些其它证明，PFR证明必须依赖于几个先前的证明。

因此，存在一个依赖图，它们的颜色取决于你是否已经形式化它们。绿色圈是一个已经用形式化证明的，蓝色圈是尚未被形式化证明，但已准备好被形式化，比如所有定义都已到位。白色圈，即使证明还没有被形式化，必须有人编写。

因此，你得到了这个任务树，而这个项目的美妙之处在于你可以让所有这些人独立地在这张图的不同部分上协作。

参与者中有些人甚至不是数学家，他们是计算机程序员，但他们非常擅长做这些小型拼图式的事情。每个人都选择了他们认为能做的一个圈，并最终在三周内完成了整个项目，这是一个非常激动人心的项目。

你知道，在数学领域，我们通常不会与这么多人合作，我见过的最多是5个人。这是因为当你在一个大项目上合作时，你必须信任每个人的数学都是正确的，超过一定规模，这就变得不可行。

但有了这样一个项目，Lean编译器会自动检查，你不能上传任何无法编译的内容，所以你可以与你从未见过的人合作。

这是一个例子，我认为这将成为未来进行数学研究的一种越来越普遍的方式。

虽然工具正在改进且变得更加用户友好，但仍然很痛苦，且需要具备一定的编程专业知识。

另一方面，如果你需要修改你的证明，比如，这个定理中原来有一个12，后来要把12改进成11，从而得到了一个稍强一些的定理。

通常情况下，如果你这么做，你必须重写整个证明，或者尝试将12替换为11但接下来还必须检查在此过程中是否有其它错误。

但实际上，当我们对这个过程进行形式化后，只用了几天时间就把12改为11，我们只是在某个地方将12改为11，然后Lean在大约五个地方报错。

目前实际上有不少大型证明形式化项目正在进行中，也许最大的是Kevin Buzzard的项目，他刚刚获得了一笔巨额资金用于将费马大定理在Lean中形式化。

他说这个项目最重要的部分将需要五年时间来完成，但他没有声称五年内能完成全部，很有趣。

所以这是形式化证明助手的一个应用。

2.机器学习

接下来我将谈谈机器学习。

机器学习使用神经网络来预测各种问题的答案，这些答案可以在许多领域中使用。不过，我将跳过我最初讨论的使用神经网络猜测偏微分方程解的方法。

我想谈谈机器学习在结理论中的应用。

结理论是数学中一个相当有趣的领域，它汇集了许多不同的数学分支。

结就是空间中闭合的一圈绳索或曲线。如果有办法可以连续地将一个结变形为另一个结，并且在这个过程中绳索不允许自我交叉，那么这两个结就被认为是等价的。

来源：维基百科

因此，结理论中的基本问题是：两个结何时是等价的？两个结，是否有办法将一个转变为另一个？

通常解决这个问题的方法是开发所谓的结不变量。

这些可以是各种数值，有时也包括多项式，你可以将这些数值或多项式附加到一个结上，无论你如何连续变形结，这些数值都不会改变。因此，如果两个结具有不同的不变量，它们就不能被认为是等价的。

存在许多类型的结不变量。有一种称为签名的不变量，你可以平展结并计算交叉点无论交叉是向上还是向下，并据此创建一个特定的矩阵等。