最近，在英国巴斯举行的第65届国际数学奥林匹克（IMO）大会上，菲尔兹奖得主著名数学家陶哲轩的演讲为我们提供了一个深入了解AI在专业领域应用的窗口。他说尤其惊人的是虽然神经网络已经存在了 20 年，AI技术其中以大型语言模型（LLMs）为代表也已经有大约 5 年的历史，但直到最近，AI输出才慢慢达到了人类的水平。
陶哲轩指出，虽然AI暂时可能有点困难直接解决问题，但它能提供宝贵的见解，帮助研究者找到问题之间的联系，并指引深入研究的方向。这种辅助作用不仅体现在数学研究中，也反映了AI在各个领域的广泛应用潜力。
例如GPT-4，展示了令人瞩目的能力。它们不仅能在某些复杂问题上表现出色，还能作为创意和灵感的来源。陶哲轩分享了自己使用AI辅助工具解决数学问题的经历，展示了AI如何为研究提供新的思路。这种人机协作的模式正在各个领域中得到应用，推动着创新和进步。然而，正如他所强调的，我们仍然需要保持对传统方法的掌握。只有深入理解问题本质，我们才能有效地利用和指导AI。这一观点不仅适用于数学研究，也适用于我们与AI互动的所有领域。
AI技术的不断进步为无论是专业领域和日常生活中的我们带来无限可能。当前首要任务是学会如何最佳地利用这些工具，在人机协作中找到平衡，为我们自己创造更美好的未来。
(提示：本次演讲内容涉及许多数学理论）
视频时间轴
01:41 机器和数学的历史
06:11 在线整数序列百科全书
09:28 SAT 求解器
14:38 证明助理
36:05 机器学习
41:34 大型语言模型
51:11 问答一：Voevodsky
53:14 问答二：年轻时大学生活
55:10 问答三：为什么选择数学领域
文稿整理
主持人: 大家好。可能在座的一些年轻选手还不太了解陶哲轩（Terence Tao） 教授。我简单介绍一下：他11岁时首次参加国际数学奥林匹克（IMO），就获得了一枚铜牌。第二年，他又获得了银牌。接着，13岁的他赢得了金牌，成为当时最年轻的金牌得主。随后他进入了大学，不再参加 IMO 竞赛。如今，他是加州大学洛杉矶分校的教授，我可以毫不夸张地说，他是 IMO 历史上最闪耀的明星之一，也是当代最具影响力的数学家之一。
特别为大家介绍：陶哲轩教授，欢迎他。
演讲部分
1、机器与数学的历史
谢谢大家。我非常高兴能够重返 IMO。当年在 IMO 的经历是我人生中最快乐的时光之一，我至今仍然深感怀念。希望大家不仅在比赛中，甚至在社交活动中都能享受这段时光，无论成绩如何，他们总能为我们举办非常精彩的活动。
今天我的演讲主题是人工智能，更广泛来说，是机器如何辅助数学。你们可能都听说过人工智能，知道它正在改变一切。今天早些时候，DeepMind 还介绍了他们的新产品 AlphaGeometry，它现在已经可以解答一些 IMO 的几何问题了。实际上，在我演讲之后，还会有一个关于 AI 数学奥林匹克的展示，希望大家能留下来观看。
我将主要探讨这些工具如何逐渐改变研究数学，而这与竞赛数学是不同的。竞赛数学要求你在三小时内解决一个问题，而研究数学有时可能需要几个月，甚至可能需要你改变研究方向。这与数学竞赛确实不同，但两者之间也有一定的共通之处。
这确实是一个非常激动人心的时代，正在带来巨大的变革，但同时也有一种延续感。事实上，我们很久以前就已经开始使用计算机和机器来进行数学计算了，只是使用的方式在变化，但这实际上是延续了一种机器辅助的悠久传统。那么问题来了：我们使用机器来进行数学计算有多久了？答案是：几千年。这里展示的是古罗马人用来进行数学计算的机器。算盘是最早的机器之一，甚至还有一些更早的。
当然，这些机器看起来比较简单，不算特别“智能”。那么计算机呢？我们使用计算机进行数学计算又有多长时间了？大约有300到400年了。这听起来有些奇怪，因为我们的现代电子计算机直到1930年代和1940年代才出现。但计算机并不总是电子的。在此之前，它们是机械的，再往前则是人工操作的。
“计算机”其实是一种职业——指的是那些专门从事计算工作的人。这里展示的是二战期间的“计算机”团队，她们大多数是女性，因为当时男性都在前线作战。她们使用加法机进行计算，程序员负责指挥她们的工作。那时计算的基本单位不是 CPU，而是“kilo-girl”——即1000名女性工作一小时的计算量。
事实上，我们使用计算机的历史可以追溯到更早的时期，至少从18世纪开始，甚至更早。那时，计算机的最基本用途是制作表格。你可能听说过 Napier 的对数表。如果你需要计算正弦或余弦等函数值，就要使用计算机生成这些表格。我在上高中的时候，课程中还教我们如何使用这些表格，只不过这些表格已经逐渐被淘汰了。如今我们有了计算器和计算机。
即使在今天，我们仍然使用表格。在数学研究中，我们依赖表格——现在我们称之为数据库，但本质上它们还是表格。许多数学的重要发现最初都是通过表格得出的。在数论中，一个最基本的结果被称为素数定理。它大致描述了某个大数 X 之前存在多少素数。这个定理是由 Legendre 和 Gauss 发现的。尽管他们无法证明这一结果，但他们通过计算机生成了前一百万个素数的表格，并通过这些数据找到了规律。
几个世纪后，另一项重要的猜想——素数定理最终在1907年左右被证明，但数论中另一个核心问题——Birch 和 Swinnerton-Dyer 猜想同样是通过大量表格的数据发现的，这次的数据是关于椭圆曲线的。
2、在线整数序列百科全书
现在有很多数学家，包括我在内，都会使用一个名为“在线整数序列百科全书”（OEIS）的数据库。或许你自己也接触过它。你可能能记住很多经典的整数序列，比如我如果说 1, 1, 2, 3, 5, 8, 13——你立刻就能想到这是斐波那契数列。OEIS 是一个包含成千上万个类似序列的数据库。
许多时候，当数学家在研究某个问题时，会遇到一些与问题自然关联的数列。比如，可能会有一个与 n 相关的空间序列，你可以计算其维度、数量或集合的基数等。你可以算出前五、六个甚至十个数字，然后把它们输入 OEIS 中进行比对。如果运气好的话，这个数列可能已经被别人录入过，他们可能是通过研究另一个完全不同的数学问题发现了这个数列。这种关联能为你提供一个重要的研究线索，并且许多有前景的研究项目就是这样被发现的。
我们最早使用计算机的方式之一就是利用表格。提到使用计算机进行数学计算，通常想到的就是数值运算。这个正式的名称叫做科学计算。当你需要进行大量的计算时，只需交给计算机来完成。自 1920 年代以来，我们一直在做这件事。
可能第一个真正进行科学计算的人是 Hendrik Lorentz。他受荷兰政府委托研究如何建造一个巨型堤坝，他们需要预测水流的变化，于是不得不模拟流体方程。他动用了大量“人力计算机”来完成这项工作，并发明了浮点运算。他意识到，如果要让大量的人快速完成大量计算，使用浮点数来表示不同数量级的数值是非常有效的。
如今，我们用计算机来模拟各种现象。如果你要解大量线性方程组或偏微分方程，或者做一些组合计算，你同样可以解决代数问题。原则上，许多奥数竞赛中的几何问题都可以通过科学计算解决。你可以将任何涉及 10 个点、一些直线和圆的几何问题转化为一个包含 20 个未知数的方程组，然后输入到 Sage 或 Maple 这类工具中进行计算。
不幸的是，一旦问题的规模超过一定程度，计算的复杂度就会急剧增加，甚至呈现双指数级增长。所以直到最近，用标准的计算机代数软件来硬解这些问题仍然不太可行，但现在有了 AI 辅助，这种方式可能会更有效。你可能已经听过今天早上的相关演讲。
3、SAT 求解器
另一种现在非常强大的科学计算工具是 SAT 求解器（可满足性求解器）。它们用于解决一些逻辑难题。比如，如果你有 10 个命题，每个命题要么为真要么为假——可能有 1000 个这样的命题——而你知道如果第三个命题为真，第六个命题为真，那么第七个命题就必须为假。如果你有一堆这样的约束条件，SAT 求解器会尝试通过这些信息来推导出一个结论——你能否证明某个命题组合是正确的。
SAT 求解器的高级版本叫做 SMT 求解器（模理论可满足性求解器），其中你还可以引入一些变量，比如 x、y 和 z，并假设一些定律，比如加法是交换的和结合的。你把这些定律和其他已知的事实一起输入，尝试强行推导出某些结论。
这些工具非常强大，但它们的扩展能力有限。当命题数量超过千条时，这些求解器就很难在合理的时间内完成计算。但它们确实可以解决一些问题。最近的一个成功案例是解决了毕达哥拉斯三元组问题，这个问题以前一直没有得到解决，直到一个大型计算机 SAT 求解器的计算结果出来。
问题是：你取自然数，并将它们染成红色或蓝色。无论你如何染色，总会有一种颜色的数列包含一个毕达哥拉斯三元组——即三个能够构成直角三角形边长的数，如 3, 4, 5。
这个问题以前没有得到证明。我们没有这个问题的人工证明。但现在我们有了一个计算机证明。现在已知实际上你只需要考虑到 7,824 个自然数。无论你如何将这 7,824 个自然数分成两种颜色，总会有一种颜色的数列包含一个毕达哥拉斯三元组。但是有 2 的 7824 次方种分类方式——你不能通过暴力破解来解决这个问题，所以必须使用一些聪明的方法。但这是可行的。一旦超过 7,825，总会出现一个毕达哥拉斯三元组。而对于 7,824，有一个例子证明无论如何染色，都没有毕达哥拉斯三元组。
这是可以证明的。实际上，这个证明曾经是世界上最长的证明之一。虽然它现在排在第二位，但当时仍然是最长的证明之一。这个证明需要几年的计算，并生成了一个证明证书。实际证明文件大小达到 200 TB，尽管后来压缩到了仅 86 GB。
这是我们如何利用计算机来进行大规模案例分析的一个例子。这种使用计算机的方式相当直接显而易见。但近年来，我们开始以更具创造性的方式使用计算机。我认为有三种计算机辅助数学的方法特别令人兴奋，尤其是当它们与其他工具结合使用时，比如传统的数据库、表格、符号计算和科学计算。
首先，我们正在使用机器学习神经网络来发现新的数学关联，揭示出人类难以察觉的数学领域之间的关系。
最引人注目的当属大型语言模型，它们从某种意义上说是非常庞大的机器学习算法，可以处理自然语言——比如 ChatGPT 和 Claude 等工具。有时它们能提出可能的解题方法，有时有效，有时无效。你可以在我演讲之后的讲座中看到更多这样的例子。
还有一种刚刚开始被普通数学家使用的技术，叫做形式证明助手。这些工具类似于编程语言，但用于验证某个推论是否正确，能否从已知数据中得出结论。直到最近，这些工具还相当难用，但现在它们变得相对容易使用，并推动了一些有趣的数学项目，这些项目在没有这些证明助手的情况下是无法完成的。未来它们将与我今天提到的其他工具很好地结合使用。
4、证明助手
接下来，我想聊聊使用机器和计算机进行数学运算的一些现代方法，我想我会从证明助手开始讲起。
历史上第一个真正由计算机辅助完成的证明可能是四色定理的证明——这个定理证明任何平面地图都可以用四种颜色进行着色。该定理于 1976 年得以证明。那时候还没有现在所说的证明助手——如果用现代标准衡量，这甚至不能完全算作是计算机证明。它是一个需要大量计算的证明，其中一部分由计算机完成，另一部分则由人类完成。
四色定理的证明方法基本上是对国家的数量进行归纳。你需要证明，如果有一张庞大的地图，那么其中的一些子图必须包含在大约 1,000-2,000 个特殊子图之一里。这是他们需要核查的一项工作。接着，他们还需要确认，每当有一个子图时，是否可以用一个更简单的图形来替代它，并且如果这个更简单的图形可以用四种颜色上色，那么整个地图就可以上色。他们必须为这大约 10,000 个子图核实这些特性——我想这些特性叫做“可消性”和“可简化性”。其中一部分工作可以通过计算机完成，尽管当时使用的计算机还是相当早期的设备——研究人员必须手动将每个图形输入程序进行检查。另一部分工作则由人力完成——其中一位作者的女儿需要耗费数小时手动核查这些可简化性特性，工作非常枯燥乏味。
这个过程并不完美——出现了许多小错误，他们不得不多次更新表格。所以按照现代标准，这还不能算是一个完全由计算机验证的证明。直到 90 年代，才出现了一个更为简单的证明，只用了大约 700 个图形。现在，所有需要验证的特性都有一个非常清晰的定义，你可以使用你喜欢的计算机语言，比如 C 或 Python，编写代码，通过几页纸、几百行代码，用现代计算机在几分钟内完成验证。
真正要完全验证这个过程——即编写一个从数学公理出发的完整证明——是在 2005 年使用一种名为 Coq 的证明助手语言完成的。我想它现在改名为 Rooster 了。
这是最早通过计算机验证的证明之一。你会发现从这个证明首次出现到我们最终能够通过计算机完全验证它之间，存在一个巨大的时间差距。
另一个著名的例子是开普勒球体堆积猜想。这是一个非常古老的猜想，由开普勒在 17 世纪提出。问题的表述非常简单：你有一堆单位球体，想要尽可能有效地填充三维空间。
最直观的堆积方式就是三角堆积方式——类似于超市里摆放橙子的方式。此外，还有一种叫做立方堆积的方式，其密度相同。显而易见的堆积密度大约是 74%，问题是——这真的是最优的堆积方式吗？
这个问题出乎意料的难。在二维情况下，六边形堆积是最优解，这不难证明。直到最近我们才知道 8 维和 24 维空间的答案——这是 Viazovska 的伟大成就，她昨天可能已经提到过这个工作。然而，三维是我们已知的唯一一个除去一维这个显然平凡的情况之外的特例。出乎意料地难以证明。这个猜想并没有一个完全由人类能够理解的证明。有一个策略——问题的难点在于这些球体的数量是无限的，密度是一个渐近的概念，因此它并不是一个可以直接交给计算机处理的有限问题。
但是可以尝试将其简化为一个有限的问题。Toth 在 1950 年代提出了一种策略。每当你进行一个堆积，它会将空间划分为称为 Voronoi 区域的多面体。球体的 Voronoi 多面体指的是那些离球体中心最近的点。因此，你可以将空间分割成这些多面体，这些多面体有一定的体积。你还可以计算它们的表面积等数据，这些数据有一定的统计规律。
体积——例如，堆积密度与这些区域的平均体积密切相关。因此，如果你能够描述这些多面体的平均体积行为，那么至少可以得到堆积有效性的一些上限。你可以尝试建立这些多面体之间的关系——例如，如果一个多面体很大，它可能会导致相邻的多面体变得很小，因此你可以尝试找到一些将多面体的体积相互关联的不等式。你可以收集大量这些不等式，然后进行一些线性规划，希望能够推导出正确的密度值，也就是那个神奇的 π/√18。人们做了很多尝试。有些甚至宣称成功了，但这些成果没有被公认为有效的证明。
最终，这个问题由 Thomas Hales 和他的合作者解决了。他们采用了相似的策略，但进行了许多技术性的改进。他们将 Voronoi 单元替换成了更为复杂的单元，并且发明了一个叫做“分数”的概念，用于为这些单元分配分数，这个分数基于体积再加上或减去一些人为调整。
他们的目标是建立这些分数之间的线性不等式，最终得到密度的上限，并希望能准确地得到最优密度。
这种方法非常灵活——实际上，它灵活得过头了，因为有太多可能的尝试方式。有太多不同的方式可以设置这些分数。正如 Sam Ferguson 所说：“每当我在尝试最小化函数时遇到问题，我可以随时调整分数再试一次。”但这样一来，之前已经验证的部分又要重新来过。结果是得分函数变得越来越复杂。他们在这项工作上花了将近十年的时间，每次调整都意味着工作量从几个月增加到几年。这种不断的调整让同行们感到不满。每次我在会议上展示我的进展时，我最小化的都是不同的函数。更糟糕的是，这些函数与我之前的论文略有冲突，这需要我回过头去修补之前的工作。
但最终他们成功了。1998 年，他们宣布最终找到了一个符合 150 个变量线性不等式的得分函数，并成功最小化了它。
最初他们并不打算将此作为一个计算机辅助的证明，但随着项目的复杂性增加，他们不得不依赖更多的计算机。以 1998 年的标准来看，这个证明是庞大的。它包含 250 页的笔记和 3 GB 的计算机程序和数据。在同行评审过程中遇到了极大的困难。论文被送到顶级期刊《数学年刊》（Annals of Mathematics），并花了四年时间由 12 位审稿人进行评审。最终审稿人表示，他们有 99% 的把握认为这个证明是正确的，但无法完全验证计算机计算的准确性。编辑们做了一件非常不寻常的事——他们发表了论文，并附上了一个编辑声明。后来，这个声明被移除了。当时，对于计算机辅助证明是否可以被视为真正的证明，存在很大的争议。现在，我们对这种证明已经更加接受了。
即便如此，论文发表后仍然存在是否真正构成证明的疑虑。因此，这可能是第一个重大且高调的问题，驱使人们有强烈的动机将其完全形式化，使用形式证明语言进行彻底的验证。
实际上，Hales 开发了一种语言——更确切地说，是对现有语言的修改，用于完成这一任务。他称之为 Flyspeck 项目。他起初估计需要 20 年才能将他的证明形式化，但实际上在 21 位合作者的帮助下，仅用了 12 年时间就完成了。这一成果最终在 2014 年发表。
因此，现如今我们对这一结果充满信心，但这一过程相当艰难。
近年来，我们已经摸索出了一种更好的形式化工作流程。虽然仍然繁琐，但正在逐渐改善。Peter Scholze 是一位非常杰出的年轻数学家——比如说，他是菲尔兹奖得主。他因多项成就而闻名，但他创造了一个极具潜力的数学领域，称为“凝聚态数学”。它将代数、范畴论等数学工具运用于泛函分析——例如巴拿赫空间等函数空间理论，而在分析学中，泛函分析长期以来难以接受代数方法。
但从理论上讲，这一领域有可能使人们能够用代数方法来解决某些类型的泛函分析问题。所以他建立了一个新的范畴，称为凝聚阿贝尔群和凝聚向量空间。我不会详细解释“凝聚”的含义。他的论点是，我们在研究生课程中学习的所有函数空间范畴都不够自然——有些范畴具有更好的性质。他构建了这一理论，但有一个至关重要的“消失定理”需要证明。我在这里提到了它，但我不会解释这些词语或符号的具体含义。这是一个非常技术性的消失定理，他需要计算一个特定范畴的群。如果这个定理无法成立，整个理论将失去实际意义。这几乎是整个理论的基石。
他在博客中谈到了这一结果。他提到自己花了一整年的时间沉迷于这个定理的证明，几乎因此崩溃。最终他们勉强把论证写了下来，但没有人敢去详细检查，因此他仍然心存疑虑。
“这个定理决定了凝聚形式主义是否能有效应用于泛函分析。这一论断至关重要，所以仅有 99.9% 的确定性是不够的。”他表示，尽管很高兴看到世界各地有很多关于凝聚数学的学习小组，但这些小组的研究往往在面对这一定理时止步不前。“这个证明实在不够有趣。”他说，“这可能是我迄今为止最重要的研究成果——所以必须确保它的正确性。”
因此，他也极其有动力去将这一定理形式化，现在采用了一种更现代的证明助手语言——Lean。Lean 是近年来得到大量发展的语言之一，它的特点是有一个由众多数学家共同开发的庞大数学库。与从数学公理推导一切相比——随着研究深入，这变得非常繁琐——Lean 的数学库已经包含了许多中间结果，例如你在本科数学课程中会学到的内容，比如微积分、群论或拓扑学的基本定理等。
这些内容已经被形式化，因此现在有了一个现成的基础——研究不再是从公理开始，而是从研究生水平的数学教育开始。虽然离目标还有不小的差距，但这已经是一个很大的帮助。
但为了形式化这个定理，他们不得不添加许多额外的内容。数学库尚未完全完善——实际上，它仍然不完整。还有许多数学领域，如同调代数、层理论、拓扑理论等，需要被添加到库中。但仅用了 18 个月，他们就成功将这个定理形式化。
证明基本上是正确的。虽然存在一些小的技术问题，但并没有发现什么大的问题。他们还找到了一些更简洁的证明方法。有些技术步骤实在过于复杂，难以形式化，因此他们不得不寻求一些捷径。不过，这个项目的真正价值更多体现在间接影响上。首先，他们大大扩展了 Lean 的数学库。现在，这个数学库能够处理更广泛的抽象代数问题，比以往更为强大。
此外，他们还设置了一些支持软件，未来的形式化项目已经开始使用这些工具，包括我参与的一些项目。例如，在这个项目中开发的一个工具叫做“蓝图”。直接形式化一个 50 页长的复杂证明真的非常痛苦。你必须把整个证明的逻辑都记在脑子里。
但我们发现了一个更好的工作流程，首先，你可以将一个大型证明写成所谓的“蓝图”，把它分解成上百个小步骤。然后每个步骤可以分别形式化，最后只需把它们组合在一起。
所以，你把一个庞大的论证分解成许多小部分。首先撰写蓝图，然后团队中的不同成员可以各自负责形式化不同部分的论证。作为这个形式化过程的副产品，他们还生成了一个非常清晰的蓝图。如果你作为人类想要理解这个证明，蓝图可能是最好的参考资料。
这个项目的另一个衍生成果是，虽然我们现在有了这个包含数万行代码的正式证明，但现在有人试图将其转化为人类可读的证明。
另一个已经开发的工具是，你可以将用 Lean 语言编写的证明——比如这里的一个拓扑问题的证明——转化为人类可读的形式。因此，所有这些文本都是从正式证明中由计算机生成的。
它看起来像人类编写的证明。它使用了相同的数学语言，但更具互动性。你可以点击任何位置——虽然我现在不能，因为这是静态的 PDF——但在可互动的版本中，你可以点击任何位置，它会告诉你当前的假设、你正在试图证明的内容、以及变量是什么。如果某个步骤太简略，你可以展开它，它会解释这个步骤的来源，甚至可以追溯到公理。我认为这非常棒。我相信未来的教科书将以这种互动的方式编写。你首先形式化它们，然后你就可以得到比当前更具互动性的教科书。
受此启发，我自己也开始了一个形式化项目——去年我和几位合作者，包括今天在场的 Tim Gowers，一起解决了一个组合数学问题。这个问题本身并不那么重要，关键在于我们如何处理它。
我们最终完成了这个证明，整篇证明约有 33 页。我们在相对较短的时间内将其形式化——事实上，这可能是目前最快的实际研究论文形式化记录。我们用了 3 周的时间，在一个大约 20 人组成的团队项目中，使用了在 Scholze 项目中开发的所有蓝图工具。
这种形式化过程使得证明更加开放和协作。你可以得到许多漂亮的可视化图形。正如我所说，首先要做的是把大定理分解成许多小部分。
我们称这个定理为 PFR——具体为什么叫这个名字暂且不提。这个定理对应于图表底部的一个小气泡，接着我们引入了其他所有相关的陈述。PFR 的证明必须依赖于一些先前的陈述，这些陈述也依赖于之前的陈述。因此，生成了一个依赖图，不同颜色表示是否已经完成形式化。
绿色气泡表示你已经在你的语言中正式证明的陈述。蓝色气泡表示尚未形式化，但已准备好形式化——所有的定义都已准备就绪，只需有人去实际操作。白色气泡表示甚至陈述还没有形式化，需要有人写下陈述。于是，你就得到了一个任务树。这个项目的妙处在于你可以让许多人独立合作，负责这张图中不同的部分。
每个小气泡对应一个陈述，你不需要理解整个证明就可以处理自己的小部分。虽然这是一个组合数学中的问题，但贡献者包括概率论专家，甚至还有非数学背景的人，他们是计算机程序员，但擅长解决这种小型拼图式问题。每个人都选择了他们认为自己能够完成的气泡，然后完成了任务。我们在三周内完成了整个项目，这是一个非常激动人心的过程。
在数学领域，我们通常不会与这么多人合作。通常最多见的合作是五个人，因为在一个大项目中合作时，你必须信任每个人的数学计算都是正确的，而当规模达到一定程度时，这就变得难以操作。但在这样的项目中，Lean 编译器会自动检查——任何无法通过编译的内容都会被拒绝。因此，你可以与从未见过面的人合作。
实际上，我在这个项目中结识了很多人——甚至为许多项目参与者写了推荐信。这是一个例子——这是一部分证明的内容。这是 Lean 语言中证明的样子。如果你熟悉这种语言，尽管看起来有点不寻常，但它是可以理解的。这种方法实际上将证明过程分解为许多不同的独立技能。你可以让一些人负责整体布局，将问题拆解成多个小部分，然后让那些不一定了解所有数学内容的人来处理这些小部分。我认为，这将成为未来越来越普遍的数学研究方式。虽然目前操作起来还是很费力——工具在逐渐改进，变得更加友好，但你仍然需要一定的编程知识。我认为，形式化一个证明的时间可能是手写证明的十倍。
另一方面，如果你想修改一个证明——比如，在某个定理中我们原本用的数字是“12”，后来我们将其改进为“11”，得到了一个更强的结论。通常情况下，你需要重写整个证明，或者手动将“12”改成“11”，然后还要检查是否有遗漏或错误。但实际上，当我们形式化了这个证明后，再进行改动只花了几天时间。我们简单地将某个地方的“12”改成了“11”，编译器就会在五个不同的位置发出警告，提醒我们这些特定部分出现问题，然后我们就可以进行针对性的修改。因此，事实上，在某些特定类型的数学问题中，形式化方法的效率实际上更高。
现在，已经有不少大型证明形式化项目在进行。最大的项目之一是 Kevin Buzzard 的项目——他刚刚获得了一笔资助，用于在 Lean 语言中形式化费马大定理。他预计完成最重要部分的形式化大约需要五年时间。虽然他并不打算在五年内完成整个证明的形式化，但重要的部分已经在进行中了。
5、机器学习
这是关于形式化证明助手的部分。接下来，我将讨论机器学习。机器学习——这些神经网络用于预测各种问题的答案，并且可以通过多种方式使用。我想我会跳过我最初讨论的使用神经网络来猜测微分方程解的方法，这是偏微分方程领域一个非常激动人心的新工具，但我会略过这一部分。
我将讨论机器学习在结理论中的另一个应用。结理论是数学中的一个有趣领域。它将许多不同的数学领域联系在一起，但这些领域彼此之间并没有太多交集。结就是一个在空间中封闭的绳环或曲线。两个结是等价的，如果你可以通过某种方式将一个结连续变形为另一个，而不允许绳子自交。结理论中的基本问题是：什么时候两个结是等价的？如果我给你两个结，是否有某种方法可以将一个结变为另一个？
解决这个问题的通常方法是开发所谓的结不变量。这些是不随着结的连续变形而改变的各种数值，有时也包括多项式。因此，如果两个结具有不同的不变量，那么它们不能是等价的。
结不变量有很多种类型。有一种叫做签名的不变量，它计算——你将结展开并数交点，看看交点是越过还是越过某些线，然后你创建一个矩阵，等等，最终得到一个叫做签名的整数。这是一种结不变量。
还有一些著名的多项式，如 Jones 多项式和 Holmfeyer 多项式，它们与许多数学领域相关，但我不会详细讨论这些。
还有一些叫做双曲不变量的东西，它们来自几何学。你可以取结的补空间，它实际上是一个叫做双曲空间的东西。这个空间具有一定的几何结构，有距离的概念，你可以计算它的体积和其他一些不变量。
这些不变量是实数或复数。因此，每个结都有一些组合不变量，如签名，还有一些几何不变量，如这些双曲不变量。这里有一个包含各种双曲不变量的结列表——有一个叫做双曲体积的东西，还有同调尖点形状等。这些是实数或复数，但没人知道它们之间有什么联系。这两种统计结的方法之间没有任何关联。
直到最近，人们开始使用机器学习来解决这个问题。他们创建了数百万个结的数据库，这本身就是一个稍微复杂的任务，并用这些数据训练了一个神经网络。他们发现，在神经网络经过训练后，如果你给它所有的双曲几何不变量，它在约 90% 的情况下可以正确预测出签名。
这就相当于一个“黑箱”，神经网络可以告诉你签名是如何隐含在这些几何不变量中的，但它不会解释具体的过程——它只是一个黑箱。
即便如此，这仍然非常有用，因为一旦有了这个黑箱，你可以对其进行各种操作。接下来，他们进行了非常简单的分析——这被称为“显著性分析”。这个黑箱的操作方式是，它接收大约 20 个不同的输入，每个输入对应一个双曲不变量，然后产生一个输出——即签名。一旦你有了这个黑箱，你可以调整每个输入，观察输出的变化。
他们发现，在这 20 个输入中，只有三个输入对输出有显著影响。其他 17 个几乎没有什么影响力，而且这三个重要的不变量并不是他们原本预期的。例如，他们以为体积会非常重要，但实际上体积几乎无关紧要。
这三个关键的不变量是：纵向平移，以及子午线平移的实部和虚部。一旦确定了这些重要的不变量，他们就可以直接绘制签名与这三个特定输入之间的关系图，然后通过人眼观察——而不是依赖神经网络——从中发现显而易见的模式。
通过观察这些图表，他们实际上能够对问题的实质提出猜测。他们根据这些观察提出了一个猜想，但结果证明这个猜想是错误的。然而，他们利用神经网络的分析来证实这一点，并通过修正错误的方式，最终找到正确的猜想，成功解释了这种现象。接着，他们就能够证明这一猜想。因此，他们提出了一个理论解释，说明为什么签名与这些特定的统计量存在密切的联系。
我认为这是一种机器学习在数学中越来越多地被使用的方式。它不会直接解决问题，但会给出有价值的提示，帮助我们找到问题之间的联系，并指引我们在哪里进行深入研究。但最终，还需要人类来完成这些推理和连接。
6、大型语言模型
最后，我们来说说大型语言模型，它们无疑是最引人注目、引起最多关注的。虽然神经网络已经存在了 20 年，大型语言模型也已经有大约 5 年的历史，但直到最近，它们的输出才达到了接近人类的水平。
你们可能都听说过 GPT-4，这就是当前 ChatGPT 所使用的模型。当 GPT-4 发布时，有一篇论文描述了它的能力，研究人员向它提供了一个 2022 年国际数学奥林匹克（IMO）的题目。虽然这个题目是稍微简化过的版本——如果你熟悉 2022 年的 IMO，你可能会注意到它的形式与原题有所不同，但问题的本质是相同的。对于这个题目，GPT-4 实际上给出了一个完整且正确的解答，成功地解决了这个 IMO 题目。然而，这其实是一个精心挑选的例子。研究人员测试了数百个 IMO 水平的问题，成功率大约只有 1%。所以他们能够解决这个特定的问题，并且需要以特定的方式格式化问题才能得到正确的答案，但这依然非常令人惊叹。
有趣的是，这些工具在处理人类觉得难的问题时，有时表现得非常出色，但在人类认为简单的问题上，AI 却经常犯错。它的解决问题方式与人类非常不同。在同一篇论文或演讲中，他们让同一个模型进行一个简单的算术计算：7 * 4 + 8 * 8。模型根据输入猜测最有可能的输出，得出了答案是 120。然后它停顿了一下，说“也许我应该解释一下为什么答案是 120。”于是它开始一步步计算，结果得出了实际的答案是 92，而不是最初的 120。如果你质疑它“等等，你之前说是 120”，它会回答“哦，那是个错误，抱歉，正确答案是 92。”
所以你可以看到，AI 并不是从基本原理出发来解决问题的，而是在每一步中猜测下一个最自然的输出。令人惊讶的是，有时这种方法奏效，但很多时候并不奏效。如何让它变得更准确，目前还在不断探索中。
人们正在尝试各种方法。你可以将这些模型与其他更可靠的软件连接起来。事实上，在接下来的演讲中，你会看到一个大型语言模型的例子，在这个例子中，你不需要自己进行计算，而是将其交给 Python 来完成。
另一种方法是强制语言模型只能生成正确的答案，方法是要求模型以某种证明助手语言输出，如果它无法编译，就返回给 AI 重新尝试。
或者，你可以尝试直接教它解决 IMO 问题的常用技巧——比如尝试简单例子、反证法证明、逐步推导等。人们正在尝试各种方法。虽然目前它还远不能解决大多数数学奥林匹克问题，更不用说数学研究问题了，但我们正在取得进展。
除了能够直接解决问题外，语言模型作为灵感来源也是有用的。实际上，我自己也使用过这些模型。我在处理某个组合数学问题时尝试了几种方法，都没有成功。于是，我作为实验问 GPT“你会建议哪些其他技术来解决这个问题？”它给了我一份包含 10 种技术的列表，其中 5 种我已经尝试过，或者显然不适用。但有一种技术我没有想到，那就是针对这个特定问题使用生成函数。当它提出这个建议后，我意识到这确实是正确的方法，但之前我忽略了。
所以，作为一个交流的对象，这种模型是有一定帮助的。虽然现在它还不是特别强大，但也并非毫无用处。还有一种 AI 辅助工具在证明助手领域变得非常实用。正如我之前提到的，编写形式化证明是一项非常繁琐的工作。就像使用任何严苛的编程语言一样——你必须完全正确地使用语法，如果错过了某个步骤，代码就无法编译成功。不过，现在有一些工具——比如我使用了 GitHub Copilot，你可以先写出部分证明，它会尝试猜测下一行代码的内容。大约有 20% 的时间，它的猜测会比较接近正确，然后你可以选择接受它的建议继续进行。
在这个例子中，我试图证明某个陈述，灰色部分是 Copilot 建议的代码。结果显示，第一行没有用，但第二行（虽然你可能看不到）实际上解决了这个问题。所以，你不能盲目接受 Copilot 的建议，因为它的输出不一定总是正确的。但如果你已经大致了解代码的工作原理，这个工具确实可以节省你很多时间。
这些工具在不断进步。目前，如果一个证明只有一两行长，它们可以自动填充。现在也有一些实验，试图让 AI 提出一个证明，然后将其反馈给编译器。如果编译不通过，你就把错误信息返回给 AI，让它重新尝试。通过这种方法，我们已经能够证明一些四到五行长的证明。
当然，对于大的证明，通常会有成千上万行代码，所以目前我们还远未达到可以立即自动形式化证明的地步。但这已经是一个非常有用的工具了。
那么，我们现在处于什么阶段呢？有些人希望在未来几年内，我们能够使用计算机直接解决数学问题。我认为我们距离这一目标仍然很遥远。对于非常专门的问题，你可以设计特定的 AI 来处理，但即便如此，它们也不总是完全可靠的——尽管可以提供帮助，但仍有局限性。
不过，至少在未来几年里，这些工具将成为非常有用的助手，超越我们目前熟悉的暴力计算辅助。人们正在尝试各种创造性的方式。
我特别感兴趣的一个方向虽然还没有取得显著成功，但未来 AI 可能会非常擅长生成有价值的猜想。我们已经在结论中看到了一些初步的例子，AI 能够猜测两个不同统计量之间的关系。所以，希望将来你可以创建庞大的数据集并将其输入 AI，然后 AI 可以自动生成许多不同数学对象之间的联系。我们目前还不完全知道如何实现这一点，部分原因是缺乏足够庞大的数据集，但我认为这是未来可能实现的目标。
我还对另一种可能性感到兴奋——这是目前还不存在的一种数学研究方式。现在，由于证明定理是一个如此繁琐且耗时的过程，我们通常一次只能证明一个定理，或者如果效率高的话，可能证明两三个定理。但随着 AI 的进步，你可以想象在未来，不再只是解决一个问题或证明一个定理，而是处理一类有 1,000 个类似问题的集合。你可以对 AI 说，“好吧，尝试用这种技术解决这 1,000 个问题。”然后 AI 会给你反馈：“用这个技术我可以解决 35% 的问题。用另一个技术呢？可以解决多少？”如果结合两种技术，可能解决的比例又会增加。你可以开始探索问题的整体空间，而不再是逐一解决每个问题。
这种方式在现在几乎是不可能实现的，或者需要几十年时间，通过大量论文逐步摸索出各种技术的应用范围。但有了这些工具，你将能够在一个前所未有的规模上进行数学研究。因此，我认为未来会非常激动人心。我是说，我们依然会以传统的方式证明定理。事实上，我们必须这样做，因为如果我们自己不掌握这些技能，就无法有效引导 AI。然而，我们将能够实现许多当前无法完成的事情。
好吧，我想我就说到这里吧。非常感谢大家。不知道大家有没有什么问题？
我们时间紧迫，但我被告知我们还有时间回答大约三个问题。所以如果有问题的请举手——那边那位。
Q&A环节
问答 一：Voevodsky
问：谢谢。您能听见我说话吗？谢谢你的精彩演讲，尤其是关于形式化数学的部分我非常喜欢。不过，您没有提到的是 Voevodsky，他因为在代数几何中的一个错误而离开了这个领域，并开始研究形式化同伦类型论。我想了解您是否研究过这个领域，并对此有任何看法。
答：对，关于 Voevodsky，他确实担心某些数学领域可能会出现危机，包括他自己创立的一些领域，因为这些领域的证明过于抽象和复杂，难以完全验证它们的正确性。
是的，因此他提出要将数学的基础转向同伦类型论，这种理论更加稳健。比如，即使你改变了数学的基本公理，在这种理论下证明的许多结果仍然是有效的。确实有一些基于同伦类型论的证明助手语言。而 Lean 并不是这样设计的，因为 Lean 的目标是形式化许多传统数学，而这些数学并不是用这种语言表达的。我确实希望未来会有多种证明助手语言，各自有不同的优势和劣势。目前，我们还没有自动将一种语言中的证明翻译成另一种语言的方法。我认为在这一点上，AI 会非常有用。一旦实现了这种能力，无论你对数学基础的哲学观点如何，我们都可以将一种语言形式化的证明翻译成另一种语言，希望这样每个人，包括 Voevodsky 在内，都会对此信服。
总的来说，形式化数学有多种方法，我们不应该急于固定在某一种标准上。
问答二：年轻时大学生活
问：好吧——嗯，这是一个随机的话题。好吧，这与今天的演讲主题不完全相关，但最近我在申请博士学位时，教授们给我的建议基本上是“时间越长越好”。似乎有一种普遍的观点认为，数学家需要在时间的沉淀中逐渐成长为能够处理重大课题的人物。从这个角度来看，你是如何看待自己在这么年轻时就进入大学的决定的？你认为这对你作为数学家和个人的成长有什么影响？
答：嗯，我——是的，我在高中、本科和研究生阶段都有一些非常好的导师。我不认为这是一场竞赛。我认为，当你准备好时，你就去上大学。你不应该因为别人告诉你需要多少年才能完成某件事而去做。
我认为这是因人而异的。对我来说，这非常重要。我是在 13 岁时进入本科阶段的，但那所大学离我家非常近，所以我仍然和父母住在一起，他们实际上开车送我去上大学的课程。如果没有这样的支持，我可能不会有一个好的体验。所以这真的取决于个人情况。是的，我确实在非常年轻的时候上了大学——但这并不意味着每个人都应该这么做。这个问题没有标准答案。
问答三：为什么选择数学领域
问：考虑到您在众多数学领域都有贡献，您是如何选择下一个研究主题和想要解决的问题的？另外，您的埃尔德什数（Erdős number）是多少？
【注：埃尔德什数是数学界用来衡量一个数学家与已故著名匈牙利数学家保罗·埃尔德什（Paul Erdős）关系近远的一个指标。埃尔德什本人的埃尔德什数为0。直接与埃尔德什合作过的数学家的埃尔德什数为1，与埃尔德什数为1的数学家合作过的人的埃尔德什数为2，依此类推。埃尔德什数为2意味着该数学家与埃尔德什有着相当近的学术联系。】
答：我的埃尔德什数是2，这很容易回答。但说实话，我并不太清楚如何选择研究主题。在职业生涯早期，通常是导师给我建议问题。现在，很多时候都是机缘巧合。数学其实是一项非常社交化的活动。我们经常参加各种学术活动。比如这次活动之后，我就要去爱丁堡参加一个数学会议，会和很多人讨论一个与PFR猜想相关的领域。很可能在那里我会进行一些有趣的数学对话，也许会由此产生一些研究问题。我确实有一些长期项目是我想解决的。但越来越多地，我发现研究问题往往源于与其他数学家的交谈。举例来说，直到两年前，我都没想到自己会谈论这么多关于人工智能的内容。我认为人们应该更加灵活。未来仍然会有人专注于某一特定领域，成为该领域的世界级专家。但我觉得，越来越多的人会随着时间推移在不同领域间转换，每隔几年就通过与他人交流发现有趣的新数学领域。
暂无评论内容