陶哲轩IMO演讲全文：一次性解决一千个问题，AI让数学摆脱蛮力计算
机器之心报道
机器之心编辑部
在探索「数学之美」的路上，人工智能到底走到哪一步了？说到这个话题，可能没人比数学家陶哲轩更懂。他几乎是最常用 AI 辅助证明的数学家之一，还在今年的 AI 数学奥林匹克竞赛（AIMO 进步奖）担任了顾问委员。
最近，在 IMO 2024 的一场演讲中，陶哲轩全面回顾和展望了计算机与人工智能在数学研究中应用范式的演变。
视频链接：https://www.youtube.com/watch?v=e049IoFBnLA
为期一个小时的演讲中，他从早期计算工具讨论到现代机器学习和形式化证明助手的演变过程，还着重介绍了最近取得的突破和面临的挑战。陶哲轩强调，虽然人工智能在数学领域的作用越来越大，但人类的洞察力和创造力对于在该领域取得有意义的进展仍然至关重要。
以下是陶哲轩演讲全文：
谢谢！回到 IMO 我很开心，在 IMO 的那段时间是我一生中最快乐的时光之一。现在回想起来，仍然觉得很美好。我希望大家都能玩得开心，无论你是否取得了好成绩，不仅仅是在比赛中，在社交活动中也是如此。
我的演讲主题是人工智能，更广泛地说，是如何用计算机辅助数学。你们都听说过人工智能以及它如何改变一切。今年早些时候，DeepMind 发布了一款新产品 AlphaGeometry。因此，这场演讲我将更多地讨论这些工具如何开始改变数学研究。
数学研究不同于数学竞赛，解决一个问题不止需要 3 个小时，而是需要几个月。有时，你解决不了问题，就必须改变问题。虽然在技巧上有一些重叠，但这与数学竞赛绝对不同。因此，AI 的加入太令人兴奋了，而且具备变革性。
但另一方面，这也是一种连续性。我们使用计算机和机器进行数学运算已经有很长一段时间了。即使做数学的方式和性质正在发生变化，但我们实际上是沿袭了机器辅助的悠久传统。
那么，有个问题：我们使用机器进行数学运算有多久了？
答案是数千年。这是罗马人用来做数学运算的机器，它不是很灵巧。
计算机呢？我们用计算机做数学题有多久了？大约有 300 到 400 年。有点奇怪吧，因为现代计算机直到 20 世纪 30 年代和 40 年代才出现。在此之前，计算机并不是电子的，而是机械的，再之前，它们是「人类」。「计算机」实际上是一种职业，是「计算的人」。
这是世界大战期间的「计算机集群」，用来计算弹道等等。这些计算机通常都是女孩，因为男人们的工作是打仗。还有一些程序员，他们负责告诉女孩们该做什么。那时计算能力的基本单位和 CPU 无关。
所以，一千个女孩这样工作一小时，能完成多少计算量？
正如我所说，我们使用计算机的历史可以追溯到 18 世纪甚至更早。在那个时代，计算机最基本的用途就是建立表格。我上高中时还在课程中学习如何使用这些已被淘汰的表格。
当然，现在我们有了计算器和电脑。现在我们仍然使用表格。在数学研究中，我们依赖表格，即使现在叫它们数据库，但本质上是一个东西。
数学领域的许多重要成果都是通过数论中的表格首次发现的。数论中最基本的成果之一叫做素数理论。Legendre 和 Gauss 发现了它，虽然无法证明这一点，但他们推测这是真的。
在数论中有一个非常核心的问题，叫做伯金 - 斯旺顿模猜想（（Birch and Swinnerton-Dyer），我想在这里谈谈。
这个猜想也是通过大量的表格发现的。现在，包括我在内的很多数学家都在使用一个表格，叫做「整数序列在线百科全书」（Online Encyclopedia of Integar Sequences，OEIS）。也许你也会遇到它，你可能会认出很多整数序列。
比如我告诉你 1,1,2,3,5,8,13 这个序列，OEIS 就是一个包含数十万个类似序列的数据库。
很多时候，数学家在研究一个问题时，都会涉及到一些数字的自然序列。例如，也许有一个取决于 n 的空间序列，你可以计算出这些数字中的前五六个或前十个，然后将其放入 OEIS 中进行比较。
如果你运气好的话，这个序列已经被别人放在那里了。它可能来自于一个完全不同的来源，比如是对其他数学问题的研究。这就给了你一个很大的线索 —— 两个问题之间存在着联系，许多研究都是这样产生的。
表格就是我们最早使用计算机的方法之一。当你想到用计算机来做数学题时，你会想到数值运算，它是可持续计算的正式名称。你想要做一个非常庞大的计算，就需要做很多很多的算术运算。
把它输出给计算机，我们从上世纪 20 年代就开始做了。也许第一个真正进行科学计算的人是 Hendrick Lorentz。他的任务是建一个巨大的像办公室一样的东西，他们想知道水流的内部是怎么回事，所以他们必须建立一些流体方程模型。
他用了一大堆人类计算机来解决这个问题，且不得不发明了浮点运算来完成这项工作。他意识到，想让很多人快速完成大量计算，应该用浮点来表示大量不同大小的数字。
当然，我们现在用计算机来建模各种事物，比如解决大量线性方程或偏微分方程，做一些商业计算。它还可以解决代数问题，许多几何题原则上也都可以通过科学计算来解决。
不幸的是，一旦它的计算规模增加，其复杂性就会变成指数级。因此，直到最近，用计算机代数软件蛮力解决这些问题还不太可行。但现在有了人工智能系统，这件事也许就更有希望了。
另一种已变得相当强大的科学计算是所谓的 SAT 求解器。它们基本上可以解决逻辑难题。比如，如果你有 10 个陈述或者 1000 个陈述都是真的或假的，而你知道，如果第 3 个陈述是真的，第 6 个陈述是真的，那么第 7 个陈述一定是假的。如果给你一大堆这样的限制条件，SAT 求解器就会尝试接受所有这些信息，然后总结：你能证明这些句子的某种组合吗？
SAT 求解器还有一个更花哨的版本，叫做 SMT 求解器。在这里，你还会有一些变量 x、y 和 z，你还会假设一些法则。但不幸的是，它们的规模也非常大，根本无法很好地扩展。同样，解决这些问题的时间和复杂度也会呈指数级增长。一旦超过 1000 个左右的命题，就很难在任何合理的时间内运行这些。
但它们实际上可以解决一些问题。比如最近的一个成功案例，如图所示，可能只有计算机才能解决，我认为只凭一个人根本解出不来。
这就是所谓的毕达哥拉斯三元组问题，在大型计算机服务器计算之前，这个问题一直没有解决。
问题是，你把自然数染成两种颜色：红色或蓝色，但无论你如何给这两个自然数着色，其中一种颜色都必须包含一个毕达哥拉斯三元组 A、B、C 三个数。
现在我们知道了，事实上并不需要穷举，只需要查到 7824。
这个证明需要 7 个 CPU-year 计算。他们生成了 200 兆字节，后来被压缩到 68 千兆字节。这就是我们利用计算机进行大量案例分析的一种方式。
但近年来，我们开始用更有创意的方式使用计算机。因此，有三种方式可以利用计算机进行数学运算。我觉得我真的很兴奋，尤其是当它们相互结合，并与更经典的数据库 —— 表格和符号计算，这种科学计算结合在一起的时候。
首先，我们利用机器学习和较新的网络来发现新的联系，并找出不同类型数学之间的关联方式，而这些方式是人类无法看到或不太可能看到的。
尤其是大型语言模型，某种意义上说，它是机器学习的大型版本，是一种可以使用自然语言的算法，比如 ChatGPT 等。它们可以生成可能的证明、解决问题的方法，这些方法有时有效，有时无效。在我之后的演讲中，你会看到更多这样的例子。
不过，还有另一种技术刚刚被日常数学家所使用，这就是所谓的形式化证明辅助。计算机语言是用来编写可执行代码的，而形式化辅助证明则是用来检查事物的语言，用来检查某个论证是否真实，是否能从数据中得出结论。
这些语言使用起来相当烦人，而现在它们变得越来越容易上手了。它们促进了许多有趣的数学项目，如果没有这些证明辅助工具，这些项目是不可能完成的，而且它们将来会与我在这里介绍的其他工具结合得非常好。
所以，我想谈谈使用机器和计算机辅助数学研究的新成果。从证明辅助开始吧。是的，历史上第一个真正意义上的计算机辅助证明可能是四色定理的证明，即「任何一张地图，只用四种颜色，就能让相邻的国家染上不同的颜色」。
1976 年那时，还没有辅助证明。实际上，当时做的尚不能称之为计算机证明。如今，这是一个需要大量计算的证明，其中一半由计算机完成，一半由人类完成。
他们证明四色定理的方法是：你基本上可以归纳出国家的数量，并证明如果你有一个庞大的地图，其中有一些国家的子图，那么就会产生一个大约有 1000 到 2000 个特殊子图的列表。
其中有一些工作他们可以通过计算机完成，但也不得不手工将每张图表输入程序并进行检查。这项任务实际上是由人工计算机完成的，其中一位作者的女儿不得不花上几个小时手动检查。工作非常繁琐，而且过程并不完美。有很多小错误，他们不得不更新表格。因此，这并不是现代计算机证明的标准，计算机可验证的证明是在九十年代才出现的，当时只用了 700 多个图就得到了一个更简单的证明。
但现在，所有需要检查的东西，都可以通过一种非常精确的方式找到属性列表。你可以用你喜欢的计算机语言（C 或 Python 或其他语言）编写代码，用几页纸和几百行代码就能检查出来，几分钟就能搞定。然后再实际检查它是否完全正确，并提供一个一直到数学公理的证明。
从证明首次出现，到我们可以用计算机完全验证，这中间有一个巨大的鸿沟。
另一个有名的例子是开普勒猜想。说起来非常简单。即如何在三维空间中最有效地堆叠球体，以最大限度地填充空间。如下展示了一种「三角形」的堆积方式，它看起来就像水果店里堆着的橘子一样。还有一种对偶的立方堆积方式。两种堆积方式的密度是相同的，都约为 74%。
问题是，开普勒猜想，这个难题困扰了数学家几个世纪。二维空间的最佳堆积并不难证明。但拓展到 24 维度，我们直到最近才得出答案，乌克兰女数学家 Viazovska 最近解决了这个问题。
有一种证明开普勒猜想的策略，虽然堆叠的球的数量是无限的，但我们可以先试着把它简化成一个有限的问题，用电脑来处理。
匈牙利数学家 Tóth 在 50 年代提出了一个重要的想法，即将开普勒猜想的证明转化为一个有限的组合问题。每次堆积时，空间会被细分成一些称为「沃罗诺伊区域」的多面体。这些区域是通过找出哪些点更接近某个球体而不是其他球体来确定的。
可以通过计算「沃罗诺伊区域」的体积等属性，进一步得知球体在空间中的排列密度。因此，如果你能算出这些多面体的体积在平均上如何变化，那么就可以估算堆积密度的最大值。你还可以尝试找出这些多面体之间的关系，比如，如果一个多面体非常大，可能会导致附近的多面体非常小。
因此，你可以试着找到一些不等式，基于这些不等式，进行线性规划等数学运算，最后得出了一个正确的值。然而，尽管许多人尝试了这种方法，有些甚至声称成功了，但没有一个被公认为是正式的证明。
这个问题最终首先由 Thomas Hales 和他的合作伙伴 Ferguson 解决了。他基本上采用了与前人相同的策略，但在技术层面做了很多调整，比如他没有直接计算多面体体积，而是发明了一种评分系统，通过对每个单元进行科学评分来优化计算。
这些评分基于体积并进行了微调，目标是通过线性不等式约束不同单元的得分，最终计算出密度的最大值，从而得出开普勒猜想在三维中的答案。
这种方法非常灵活，但也因为过于灵活，导致有太多变量，比如设置评分的方法等。这也把问题搞得更复杂了。
Hales 和 Ferguson 意识到，一旦计算函数的最小值时出了问题，就得改变得分函数，从头再来。但这样一来，所有已经检查过的工作都得重做。于是，评分系统变得越来越复杂。他们在这方面的工作持续了将近十年，每改一次都需要花费数月来调整。
Hales 在一篇文章中曾写道：「这种不断调整的做法并不受同行们欢迎。每当我在学术会议上展示自己的新成果，我总是在展示不同函数的最小值。而且更糟糕的是，新函数与我之前的论文不完全兼容，因此我不得不回去修改和补充早期的工作。」当然尽管如此，他们最终还是证明出来了开普勒猜想在三维中的答案。
起初，他们并不打算用计算机辅助证明，但随着项目越来越复杂，他们不可避免地越来越多用到计算机。按照当时的标准，这个证明的规模极为庞大。到 1998 年，整个证明包括了 250 页的笔记以及 3GB 的计算机程序和数据。
同时，使用计算机导致 Thomas Hales 的论文难以通过审查。Hales 把论文提交给了数学顶级期刊之一《数学年刊》（Annals of Mathematics），整个审稿过程持续了四年，审稿委员会包括 12 名审稿人。最终，他们表示 99% 地确定证明是正确的，但无法完全确认其中的所有计算。出于这种不确定性，编辑们采取了非常罕见的做法，发表了论文，并附上了一个来自编辑的保留说明，提醒读者有未完全验证的部分。不过后来，这个保留说明被移除了。
当时，关于计算机辅助证明是否可以被视为真正的数学证明存在相当大的争议。即使在论文发表后，仍有一些数学家质疑这是否真正构成一个完整的证明。
这可能是第一个用计算机辅助数学证明的大事件。这促使数学家们开始推动如何将证明过程完全形式化。Thomas Hales 因此创建了一个项目 ——「Flyspeck」，基于已有的计算机语言，他带领团队构建了一种适用于数学证明的语言，来形式化他的开普勒猜想证明。
起初，他估计这一过程需要 20 年，但在 21 位合作者的帮助下，他在 12 年内完成了，并在 2014 年正式发表。如今，我们对「Flyspeck」充满信心。即便整个过程非常艰难，在过去的几年中，我们仍在逐渐摸索出一种更好的工作流程来形式化证明。
彼得・朔尔策（Peter Scholze）是一位非常杰出的年轻数学家，曾获得菲尔兹奖，他因许多成就而闻名，其中之一就是他创造了一个极具潜力的数学领域，称为「凝聚态数学（Condensed Mathematics）」。这个领域结合了代数、范畴论等工具，应用于泛函分析的理论，如度量空间等。在泛函分析中，传统上比较抗拒代数方法的应用，但凝聚数学原则上可以用代数方法解决一些关于函数空间的某些问题。
朔尔策建立了「凝聚群」和「凝聚向量空间」这一整套理论。他的主要观点是，我们在研究生课程中学习的函数空间的范畴是不正确的，或者说并非具备最佳性质的自然范畴。然而，这套理论中有一个非常重要的消失定理需要证明，尽管朔尔策没有详细解释其中的符号和术语。
朔尔策的凝聚数学理论中有一个非常难的消灭定理（vanishing theorem），涉及某个范畴论群的计算。这个消失定理是他理论的基础，如果无法证明该定理，那么凝聚数学的框架就无法发挥其应有的潜力。
他在博客中写道：自己花了一整年时间，深陷于证明这个定理的过程中，几乎因此而疯狂。最终，他把推理写在了纸上，但没有人敢详细查看其中的细节。因此，他仍然对这个定理存有疑虑。他指出，如果这个凝聚数学的表述能有效应用于泛函分析领域，那么它的意义将极为重要。然而，他也表示，99.9% 的确定性仍然不够，因为这一工作的主题具有极其基础性的作用。
他说：「他很高兴看到世界各地有许多学习小组在讨论相关竞赛事件，但他们都没有深入到这个定理的证明部分。」他表示，这趟数学旅程并不是很有趣。他还强调，这可能是他最重要的一项工作，因此必须确保其正确性。
他很希望将这个定理用更现代的语言进行形式化。他使用一种叫做 Lean 的 Preface 语言。Lean 是近年来得到广泛开发的语言，背后有一个众包的数学库开发团队。越深入和高级的数学领域证明就越显得繁琐，尤其是像这种高深的数学领域，使用 Lean 可以帮助更加简洁地形式化复杂的证明过程。
数学库已经发展成为一个核心资源，它已经证明了许多中间结果。你在本科数学课程中可能会看到的一些基础内容，比如基础微积分、群论或拓扑学的基本概念等，都已经被形式化。因此，Lean 提供了一个坚实的基础，让你不必从数学公理重新开始，而是从大致相当于本科数学教育的水平出发。尽管与更高级的数学研究还有很大差距，但这一基础已经能大大帮助复杂数学问题的形式化过程。
为了形式化这个定理，他们不得不添加许多额外的内容，因为 Lean 的数学库目前仍不完整。在数学的许多领域里，比如同调代数理论和层理论，还需要被加入到这个库中。这些高级数学工具对于更复杂的数学证明是必要的，但 Lean 目前的库还没有完全覆盖这些内容，因此需要继续扩展以支持更广泛的数学领域。
在 EMEA 项目中，仅用了 18 个月，他们就能够能用 Lean 自动化地证明这一定理，Lean 的证明基本上是正确的。他们还找到了一些简化方法。有些步骤用代码实现起来太难，因此他们被迫寻找一些捷径。这个项目带来的是长远的价值。首先，他们极大地丰富了 Lean 的数学库，能够处理大量的抽象代数了。那些为支持该项目而构建的软件，后续的项目也在用。
例如，EMEA 项目中衍生出了一种名为「蓝图」的工具。想象一下，要直接形式化一个长达 50 页的证明，确实很痛苦。你需要在脑海中保持整个证明的连贯性。
「蓝图」的界面
为此，我们找到了正确的工作流程：首先为这个大型证明编写一个「蓝图」，它将证明分解成了数百个小步骤。每个步骤都可以单独形式化，然后将它们组合起来。你首先编写这个「蓝图」，你的团队成员可以分别处理不同部分。这种拆分还让我们得到了一点启示：如果想以人类的方式阅读数学证明，「蓝图」是最佳选择。
目前，人们正在致力于将这份长达数万行的形式化证明转换回人类可读的形式。为此，已经开发了一些新工具。例如，你可以将 Lean 的格式转换成人类可读的形式。这里有一个拓扑问题的例子。这里的所有文本都是计算机根据形式化证明自动生成的，看起来和一个人类写出来的没什么差别。
它同样使用数学语言，但它的互动性更强。你可以点击任何位置，它会告诉你你当前处于哪个位置，假设是什么，你要证明什么，变量是什么。如果某个步骤太简略，你可以展开，它会解释每个词的来源。如果你愿意，还可以一直深入探索每一个细节。
我觉得这是一个很棒的想法。我相信未来的教材会以这种互动的形式编写。你先对它们进行形式化，然后就可以制作出更加互动的教材，内部内容也会更加灵活多样。
受此启发，我自己也开始了一个形式化的项目。去年，我与其他几个人一起解决了一个关于组合产物的问题。
这个证明大约有 33 页，我们在相对较短的时间内完成了它的形式化，可能依然是最快形式化的研究论文。用了三周时间，团队有 20 人左右，利用了所有已经开发出来的蓝图工具完成了这一切。总的来说，这种方法让证明过程更加开放和协作化。而且你还能获得很多漂亮的可视化图表。正如我之前提到的，第一步是把你的大定理拆解成许多小部分。我们有一个定理，称为 PFR，接下来我们会解释为什么。在这张图的底部，有一个表示「宇宙」的小气泡。
然后我们引入了所有这些其他陈述，比如说某个证明必须依赖于之前的几个陈述，而这些陈述又依赖于更早的陈述。因此，形成了一个依赖图，图中的不同颜色表示这些陈述是否已形式化。绿色的气泡表示这个陈述已经在你的形式化语言中得到了正式证明 ；蓝色的气泡表示这个陈述还没有形式化，但已经准备好进行形式化，因为所有定义都已经就位。
而白色气泡表示，连陈述都还没有被形式化，需要有人把陈述写出来。因此，这就形成了一棵任务树。这个项目的妙处在于，你可以让所有人独立合作，处理任务图中的不同部分。每个小气泡对应一个陈述，而你不需要理解整个证明，只需处理你负责的那一部分就可以了。
比如，这个问题是一个常见选择题，但参与的人中有概率论领域的专家，也有一些根本不是数学家的人。他们是计算机程序员，但非常擅长解决这类小型谜题。所以每个人都挑选了一个他们觉得自己能处理的小气泡，并完成了它。最后，我们在三周内完成了整个项目，这真的是一个非常令人兴奋的项目。
在数学领域，我们通常不会与这么多人合作，通常一个团队最多也就五个人左右。这是由于合作大型项目时，团队中每个人的数学水平都要值得信任。需要确保他们的工作都是正确的，并且达到一定的质量标准。但这一般不太可能。
但用 Lean 编译器做这种项目，它可以自动检查。上传无法编译的内容会被编译器拒绝。因此，你可以与从未见过面的人通过 Lean 合作。我在这个过程中遇到了很多人，也为在 Lean 社区遇到的伙伴写了不少推荐信。
Lean 的格式让数学家们可以更好地分工合作。
擅长 Lean 的专家可以专注于将项目的一部分转化为 Lean，不太熟悉 Lean 的数学家可以继续原来的工作，将用 Lean 将其程式化的工作留给其他人。虽然 Lean 不能做到完全精确。如果你懂这门语言，AI 给出答案是可读的，但它看起来有点单薄并且不太符合常规。但它可以把任务分解，有一些人可以从宏观角度审视整个项目，有的人可以专注于自己擅长的一小部分。我认为这种研究方式在数学领域将越来越常见。
使用这些工具仍然挺痛苦的。虽然这些工具正在降低门槛，变得对用户更友好，但我们仍然需要具备一些编程专业知识，比如改格式比手算要多花 10 倍的时间。
另一方面，比如图中的定理中有一个数字 12，在证明过程中想要把这个 12 改成 11。但是这样必须重写整个证明，或者一个一个地把 12 剪切粘贴成 11。但当我们将其程式化后，这个效率大大提高了，把 12 更改为 11 只花了几天时间。只把某处的 12 改成了 11，编译器自动在五个类似的地方报错了。
像这类工作已经不需要亲自处理了，我们直接针对它做优化。因此，对于一些特定的数学研究，通过程式化的方法实际比传统方法更快。
目前，也有相当多这种用计算机辅助的大型数学证明项目正在进行。其中最引人瞩目的应数 Kevin Buzzard 正在用 Lean 证明费马大定理，他刚刚获得了一笔巨额资助。他表示，完成这项工作的主要工作大概需要五年时间，实际上，该项目已经开始取得进展。
下面来谈谈机器学习对数学领域的应用，我先跳过用机器学习来解偏微分方程的话题，谈谈机器学习的另一个应用。数学中的「纽结理论」（Knot Theory）是一个相当有趣的领域。它是众多的数学领域的交汇处。
2021 年，Alex Davies 等人通过机器学习拓展了对「纽结理论」的新认知。
从本质来看，一个结是一个在空间中闭合的环状或曲线。如果能够通过连续的变形，将一个结平滑地转换为另一个结，且在整个过程中结不穿越自身，那么这两个结在数学上被认为是「同胚」的。这种连续变形的过程，确保了结的拓扑性质得以保持，也就是说，在拓扑学的视角下，它们的类型是等价的。
我们可以通过机器学习来自动地识别结的性质，并对其变化的过程进行一些分析，例如，对不同类型的结进行分类，或者预测结的性质，比如它们的形态是否稳定，或者预测它可能转变成什么新形状。这些知识可以扩展到材料科学、生物学等等领域，从而为这些领域带来新的见解和解决方案。
「同胚」的结
「纽结理论」中的核心问题之一便是判断两个结是否具有等价性。面对两个结，我们是否能够找到一种方式，将一个结变换为另一个？
通常，我们通过「结不变量」来解决这个问题。「结不变量」往往是一系列数字或多项式，它们与结的结构紧密相关，并且在结的任何连续变换下都保持恒定。换言之，这些数值或多项式的不变性为我们提供了一种可靠的判断标准：如果两个结的「结不变量」不相等，那么这两个结就不可能是等价的。这是一种判断结等价的定量方法。
「结不变量」也有多种类型，其中一种称为「signature」。它通过一种特定的计数方法。首先，将结展平，然后计算交叉点的数量，区分哪些线段是相互跨越的，哪些是相互位于下方的。基于这些交叉点的信息，我们可以构造一个特定的矩阵。通过进一步的数学处理，我们得到一个名为「signature」的整数。
此外，还有一些著名的多项式也是「结不变量」，如「琼斯多项式」（Jones polynomial）和「霍姆费利多项式」（HOMFLY-PT polynomial）。不过，在此我就不深入讨论这些内容了。这些多项式、不变量为我们提供了深入理解结的复杂性和多样性的有力工具。
此外，还有一种判断标准，名为「双曲不变量」（hyperbolic invariants）。它源于几何学。你可以取结的补集，被称为双曲空间（hyperbolic space）。这种空间带有特定的几何结构，具备距离的概念，并且可以度量体积和其他一些不变量，它是实数或复数，可以用来判断两个结是否等价。
表格中展示了 1991 年由 Hildebrand 和 J. Weeks 进行的关于结的双曲不变量的研究。
这里列出了一系列关于结的假设，包括双曲体积、同调尖顶形状等等，它们涉及实数和复数。然而，没人知道这两者之间有什么联系。因此，有两种独立的方式来生成关于结的统计数据，但它们之间没有关联。
直到最近，人们才开始使用机器学习来解决这个问题。他们创建了数百万个结的数据库，并用这些数据训练了一个神经网络。结果发现，训练后的神经网络，可以根据所有的双曲几何不变量来预测签名，大约 90% 的时候它可以猜对。
这就形成了一个黑箱，它能够告诉你这些几何不变量中某处隐藏了签名的信息，但却不能解释这个黑箱的内部原理。不过这仍然有用，因为一旦有了这个黑箱，你就可以进行实验。接下来他们进行了显著性分析。
这种分析的原理是黑箱接收大约 20 个不同的输入，而输出是一个签名那么你可以通过改变每一个输入，来观察输出的变化概率。20 个输入中只有 3 个对输出起了重要作用，其他 17 个几乎没有影响，而且这 3 个也不是他们最初预期的。比如，他们本以为体积会很重要，但结果显示体积几乎无关紧要。三个重要的输入是长程平移和子午线平移的实数部分和复数部分。
一旦他们确定了最重要的输入就可以直接绘制签名与这三个输入之间的关系图，然后用人的视觉网络，而不是神经网络来观察其中的明显模式。通过观察这些图，他们可以提出一些关于问题的猜想。
尽管他们最初的猜想是错误的，但他们重新利用神经网络，证明了这个猜想的错误性，并根据错误之处进行了修正，最终得出了正确的猜想，成功解释了这个现象。一旦他们得出正确的陈述，他们就能够证明这一点，说明为什么签名与这些特定的不变量有如此密切的关系。
我认为这展示了机器学习在数学中的一个应用方式，它并不直接帮你解决问题，但能提供很多有用的提示，指引你去寻找关键的联系，不过最终还是需要人类来做出真正的关联。
最后，我们来谈谈大型语言模型，它们是最引人注目、也最为人所知的。神经网络已经存在了 20 年左右，而大型语言模型大约在 5 年左右就已经出现了，但直到最近，它们的输出才接近人类水平。你们可能都听说过 GPT-4，这是 ChatGPT 的一个模型。
非常著名的是，当 GPT-4 发布时，有一篇论文描述了它的能力。研究人员给它输入了 2022 年国际数学奥林匹克（IMO）的一道题，是一个稍微简化的版本。如果你研究过 2022 年的 IMO 题目，你会发现它不是完全相同的形式，这是一个简化版本。不过 GPT-4 给出了完整且正确的解答，它确实解决了一道 IMO 的题目。
但其实这是他们挑出来的。他们测试了数百道国际数学奥林匹克（IMO）级别的问题，成功率大概只有 1%。所以虽然这道特定的问题能够被解决，但他们必须以正确的方式来格式化问题才能得到解答。不过，尽管如此，这依然相当令人惊叹。
另一个有意思的是，某些人类觉得困难的事情，AI 可能可以轻松完成。而人类觉得容易的事情，AI 却常常难以处理。这是一种非常不同的解决问题方式。有研究人员曾让模型做一个简单的算术计算，像是 7×4 + 8×8。
模型只是根据输入猜测最可能的输出，结果它猜的答案是 120。然后它停顿了一下，说：「也许我应该解释一下为什么是 120。」于是它逐步展开解答，但当它一步一步进行计算时，实际上得出了正确的答案 ——92，而不是它最初猜的 120。如果你接着问：「等等，你之前说答案是 120。」 它会回复：「哦，那是个笔误，抱歉，正确答案是 92。」
所以它们并不是通过从基本原理推导出答案，而是每一步都在猜测接下来最自然的输出是什么。令人惊讶的是，有时候这种方法有效，但很多时候却不奏效。而如何让它们变得更加准确，仍然是一个正在进行的研究课题。
所以，人们正在尝试各种方法来改进这些模型。你可以将这些语言模型与其他更可靠的软件连接起来。实际上，接下来的演示中你会看到一个大型语言模型与其他工具连接的案例。在这种情况下，你不需要自己进行计算，而是将计算外包给 Python。不过你还可以做另一件事，强制语言模型只生成正确的答案，方法是让它们输出特定的编程语言格式。如果代码不能编译，你就把它返回给 AI，让 AI 重新尝试。
或者你也可以直接教它一些解决问题的技巧，比如我用来解决国际数学奥林匹克（IMO）问题的技巧，像是尝试简单例子、反证法，或者一步一步地证明等等。人们正在尝试各种各样的方法。虽然目前我们还远远没有能够解决大多数数学奥赛问题，更别提数学研究问题了，但我们确实在不断取得进展。除了能够直接解决问题外，AI 还可以作为某种灵感来源。
实际上，我自己也使用过这些模型，并尝试各种问题。我曾遇到一个难题，尝试了几种方法都没有成功。于是，作为实验，我向 GPT 询问它会建议使用哪些其他技术来解决这个问题。它给了我一个包含 10 种技术的列表，其中大概有五种是我已经试过但明显无用的方法，还有几种也不太有帮助。
但其中有一种技术我没有尝试过，那就是对这个特定问题使用生成函数。当它提出这个建议时，我意识到这确实是正确的方向，但我之前忽略了。所以，作为一个可以交流的人，它还是有一定用处的。虽然现在并不是特别出色，但也并非完全无用。
另一个已经变得非常有用的 AI 辅助类型是用于证明辅助的工具。正如我所说，写正式的证明是一项非常繁琐的任务，就像任何非常严苛的计算机语言一样，你必须确保语法完全正确，如果你漏掉一步，它就无法编译。现在有一些工具，比如我用过的 GitHub Copilot。
你可以写下证明的一半，然后它会试着猜测下一行应该是什么。在大约 20% 的情况下，Copilot 会猜出接近正确的内容，然后你可以选择接受它的建议。比如，在一个实例中，我正尝试证明某个命题，灰色部分是 Copilot 建议的代码。结果发现第一行没什么用，但第二行却上解决了这个问题。所以，你不能完全依赖它的输入，因为它不一定能编译成功。但如果你大致了解代码的工作方式，它可以为你节省很多时间。
这些工具正在不断改进。现在，如果证明只有一两行，它们可能能够自动完成。还有一些实验在进行中，尝试让 AI 生成证明，接着将其反馈给编译器，如果编译出错，再把错误信息传回 AI。
可以看到，这种方法可以处理大约四到五行的证明。当然，一个完整的大型证明通常有数万行，因此我们还远没有达到能够立刻将证明完全形式化的水平。但即便如此，它已经成为一个相当有用的工具了。
我们现在处于什么阶段？有人希望在未来几年内，我们能够直接使用计算机来解决数学问题。我认为距离这个目标，还有很长的路要走。对于一些细分领域中的问题，我们可以构建一个 AI 专家。但它们并不完全可靠。因此，至少在接下来的几年里，AI 将大概率扮演一个辅助的角色。
除了我们熟知的那种 AI 辅助「蛮力计算」之外，我认为还有一个特别令人兴奋的方向。尽管目前还没有真正成功，但是 AI 已经非常擅长生成猜想。我们已经看到了一些例子，AI 已经可以推测两个统计数据之间的联系。所以现在我们寄希望于创建庞大的数据集，将大量数据「喂」给 AI，然后它们就会自动生成各种数学对象间的联系。其实这还并没有实现，我们还不清楚如何做到这一点。当然，我们还没做出那种大体量的数据集。但我认为 AI 能生成数学猜想在将来很有可能成为现实。
证明数学定理是一个艰难、持久的过程。我们现在一次只能解决一个问题，如果效率够高，也许你也可以同时解决两三个问题。但是当我们有了 AI，可以一次性处理 1000 个类似的问题。你可以直接告诉 AI：「尝试用这种方法解决这 1000 个问题」，我们再检查结果，可能其中 35% 的问题已经用这种方式解决了。
此外，我能够将相似的问题综合起来一并解决。这种方法允许我们对整个问题集进行探索，而不是孤立地逐个击破。这是目前无法做到的，因为它可能需要几十年的时间，通过几十篇论文，用各种技术慢慢弄清楚。目前，我们仍然需要证明老式的定理。因为我们还没找到引导 AI 自动证明的方法。
但是凭借未来强大的 AI 能力，你将真的可以开始以一种真正前所未有的规模进行数学运算，未来将会非常激动人心。