陶哲轩最新演讲：人工智能时代，数学研究将迎来前所未有的规模
编辑日期：2024年08月28日
从古至今，机器辅助计算的传统与演变一直备受关注。
近日，陶哲轩在其最新的演讲中深入探讨了AI在数学领域的应用。在2024年国际数学奥林匹克（IMO）的现场，陶哲轩进行了长达一小时的主题演讲，题目为《AI与数学》。
陶哲轩在演讲中详细阐述了他对AI与数学关系的看法，并解读了机器学习和大模型在数学研究中的应用与发展。以下是他的主要观点：
- 借助AI技术，未来有可能同时处理一系列复杂问题，从而以前所未有的规模开展数学研究。
- AI在数学研究中的应用并不仅仅是理论上的设想，陶哲轩本人也透露自己使用GPT-4寻找解题灵感，并利用GitHub Copilot辅助证明，成功率约为20%。
- 除了演讲内容外，陶哲轩近期发布的几篇帖子也聚焦于AI的应用。
网友们对陶哲轩的观点表示赞赏：
- 他没有盲目支持或反对AI的炒作，而是理性地评估了这些工具及其未来发展的可能性。
在演讲中，陶哲轩从机器辅助计算的传统出发，详细讲解了以下几个方面：
- 大家都听说过AI及其在各个领域的应用。例如，DeepMind发布的AlphaGeometry现在已经能够解答一些IMO几何问题。
我将进一步探讨这些工具如何开始改变数学研究的方式。这与数学竞赛截然不同——数学竞赛通常限定三小时来解决一个问题，而数学研究则可能需要几个月甚至更长时间。有时候，如果问题无法解决，就必须调整问题本身。这与数学竞赛完全不同，尽管两者在技能上有一定的重叠。
这一切都令人兴奋，并且已经开始产生变革性的影响。但另一方面，我们也感到一种延续性，因为我们实际上已经使用计算机和机器来进行数学运算很长一段时间了，而现在这种运算方式的本质正在发生变化。
实际上，这延续了长久以来机器辅助的传统。
那么，我们使用机器进行数学计算有多久了？答案是数千年。
这是古罗马人曾用来进行数学计算的工具，算盘是早期的一种机器，甚至还有更古老的工具。听起来可能有些乏味，这些工具并不智能。
那么，我们使用计算机进行数学计算有多久了？大约是三四百年。这听起来有些奇怪，因为你知道，现代电子计算机直到20世纪三四十年代才出现。
但在电子计算机之前，计算机是机械式的，甚至“计算机”一词也曾指代进行计算的人。这是一种职业。
过去有人力“计算机集群”，人们使用加法机来计算弹道学等问题。计算能力的基本单位不是CPU，而是kilgirl，即1000名女性在一小时内能完成多少计算任务，因为当时的男性都在前线作战。
正如我之前所说，人们很早就开始使用计算机，实际上早在17世纪甚至更早之前就开始使用了。
那时，计算机最基本的用途是制作表格（table），你可能听说过纳皮尔的对数表。
如果你想计算正弦、余弦等函数值，你会使用计算机生成这些表格。在我上高中的时候，我们仍然学习如何使用这些表格，尽管它们已经被淘汰。
当然，现在我们有了计算器和现代计算机。
我的意思是说，在数学研究中，我们过去依赖的是表格，而现在称之为数据库，但它们本质上是一样的。
在数学领域，许多重要的成果最初都是通过表格发现的。
例如，数论中的一个基本成果——素数定理，它大致描述了一个大数x之前有多少个素数。这一发现归功于勒让德和高斯等人。尽管他们当时未能证明这一点，但通过高斯和其他人使用早期的计算工具，他们推测这一理论是正确的。实际上，高斯本人就像一台计算机，通过计算表格来寻找规律。
另一个重要的例子是 Birch 和 Swinnerton-Dyer 猜想，这里不详细讨论。这个猜想也是通过查看大量关于曲线的数据表格而首次发现的。
如今，包括我在内的许多数学家都会使用一个名为 Online Encyclopedia of Integer Sequences（OEIS）的数据库，它收录了大量数学序列数据。
也许你遇到过这样的序列：“1, 1, 2, 3, 5, 8, 13”，你知道这是斐波那契数列。OEIS 就是一个包含成千上万个类似序列的数据库。
在数学研究中，数学家经常会遇到一些自然出现的数字序列，这些序列可能与变量 n 相关，比如空间的维数或集合的基数等。
你可以计算出这些序列的前几个数字，并将其输入到 OEIS 中进行对比。如果幸运的话，这个序列可能已经被别人记录下来了，而且可能是从某个完全不同的数学问题中得出的。
这样的发现可以揭示两个问题之间可能存在的联系，许多研究就是由此开始的。
机器在数学领域的一个关键应用是科学计算（scientific computation）。当你需要执行大规模的计算时，可以将大量的算术运算任务交给计算机。自20世纪20年代以来，这种方法已被广泛采用。
据说，最早进行科学计算的人之一是亨德里克·洛伦兹。当时，荷兰人计划建造一座巨大的堤坝，并委托洛伦兹计算水流的变化。为此，他们需要建立模型并求解一些流体力学方程。洛伦兹实际上雇用了一批人类“计算机”，采用浮点运算来解决这个问题。
他意识到，如果要让许多人快速完成大量计算，应该使用浮点数来表示各种不同大小的数字。如今，我们使用计算机来模拟各种现象。
如果你需要解决许多线性方程或其他类型的方程，可以进行一些组合计算，解决代数问题。许多国际数学奥林匹克竞赛（IMO）中的几何问题原则上都可以通过科学计算来解决。现在有一些代数软件包，例如，你可以将一个涉及10个点、几条直线和几个圆的几何问题转化为一个包含20个实数和20个未知数的方程系统，然后输入到Sage或Maple等软件中求解。
然而，随着问题规模的增加，解决问题所需的计算复杂度可能会呈指数级或双指数级增长，这超出了传统计算机代数软件包的能力范围。因此，直到最近，仅靠标准的计算机代数软件包来暴力求解这些问题几乎是不可能的。但借助人工智能的帮助，这种情况有望改变。
另一种强大的科学计算工具是所谓的SAT求解器，它可以用来解决某些逻辑谜题。
例如，假设你有1000个真假不定的陈述，并且你知道如果第三个陈述为真，则第六个陈述也为真，进而第七个陈述必然为假。如果你给出一系列类似的约束条件，SAT求解器会尝试利用所有这些信息，判断是否能确定某些陈述为真或为假。而更为高级的SMT求解器则可以处理带有变量如x、y、z的情况，通过输入一些规则和其他已知事实，试图在有限的假设中得出结论。
这些工具功能强大，但在面对大规模问题时却难以应对。因为问题的复杂性可能导致计算时间呈指数级增长，当陈述数量超过约1000个时，这些求解器的运行将变得极其困难。
尽管如此，计算机在某些问题上确实能够发挥重要作用。
比如，在组合数学领域的一个成功应用就是解决了一个人类几乎无法独立解决的问题，或许只有借助计算机才能实现。这个问题涉及毕达哥拉斯三元组（即满足a² + b² = c²的整数a、b、c）：
如果将自然数涂成红色或蓝色两种颜色，无论如何涂色，是否存在一种颜色包含毕达哥拉斯三元组abc？
这个问题此前一直未获解答，直到使用了一台大型计算机进行大量计算后才得以解决。
我们现在知道，无需检查所有自然数。对于1到7824之间的自然数，可以将其分为两种颜色，使得任何一种颜色中都没有毕达哥拉斯三元组；然而，对于1到7825之间的自然数，则必然会包含某种颜色的毕达哥拉斯三元组。
这个证明曾经是世界上最长的证明之一，现在则是第二长。该证明需要4个CPU年的计算时间，并生成了一个包含200TB数据的证明文件，后来被压缩至86GB。
因此，这展示了计算机解决问题的一种显著方式。
近年来，我们开始以更具创造性的方法使用计算机，特别是在将其与其他计算机、传统数据库、表格和科学计算结合方面。我们利用机器学习神经网络以不同于人类的方式发现新的关联，探索不同类型数学之间的联系。
尤为突出的是大型语言模型，如ChatGPT和Claude，它们能够进行自然语言对话，并且有时能提出有效的解决方案。
此外，还有一种被数学家们采用的技术——形式证明助手。
这些工具实际上是一种编程语言，类似于用计算机语言编写可执行代码，形式证明助手则用于验证命题的真实性，并从数据中得出结论。
最近，这些工具变得相对易于使用，并且正在支持许多有趣的数学项目，这些项目如果没有形式证明助手的帮助是不可能完成的。
未来，这些工具将与我提到的其他工具更好地结合。
因此，我想讨论一下如何使用现代计算机和机器来进行数学研究，首先从形式证明助手开始。
第一个真正意义上的计算机辅助证明可能是四色定理的证明。
该定理于1976年得到证明：任何一张地图只需四种颜色进行着色，即可确保相邻区域的颜色不同。
△ 图源维基百科
他们证明四色定理的方法主要是通过归纳国家的数量。你需要证明如果有一张大的地图，则会存在某些国家的子图。他们列出了大约1000到2000个特殊的子图，每个大的国家图在某种意义上必须包含这些子图中的至少一个，这是他们必须检查的一项内容。
然后，他们必须检查每当存在一个子图时，是否可以用更简单的结构替代该子图；如果这个更简单的结构可以用四种颜色着色，那么整个主图也能被着色。此外，还要检查这些子图的可简化性。
这些任务中的一部分可以通过计算机完成，而另一部分则需要人们花费数小时手动检查。
我认为，这是一个需要重新审视的过程，因为这个过程非常乏味，并且并不完美，还存在许多小错误。根据现代计算机证明的标准，这并不能算作一个可以被计算机验证的证明。
直到90年代，情况才有所改变，当时出现了使用约700个子图的一个较为简单的证明。
2005年，借助Coq这一证明辅助工具，实现了完全形式化的、计算机可验证的证明。
我们可以看到，从最初的证明到最终能够完全通过计算机验证之间存在着巨大的时间差距。
另一个著名的例子是关于球体最密集堆积的几何问题——开普勒猜想。
开普勒猜想指出，在三维空间中，最密集的球体排列方式是面心立方堆积（FCC）和六方最密集堆积（HCP），这两种排列方式占据的体积比约为74.048%，这是所有可能排列方式中最高的。
△ 图片来源：维基百科
如何确定这种堆积方式是否最优？这成为一个特别困难的问题，而且并没有一个完全对人类可读的证明。
问题在于，对于无限多的球体，密度是一个渐进的过程，因此这不是一个先天的有限问题，你不能仅仅将其交给计算机处理。
但你可以尝试将其简化为一个有限的问题。
每次进行堆积时，系统会将空间细分为称为Voronoi区域的多面体。每个球的Voronoi多面体包含所有距离该球中心最近的点，这些多面体具有特定的体积，可以计算它们的面数、表面积等属性，从而获取相关统计数据。Toth在20世纪50年代提出了一种策略。他发现，通过考虑有限数量的Voronoi多面体的体积，并应用某些加权不等式，可以得出球堆积密度的上界。
你可以尝试分析这些多面体之间的关系，例如，如果一个Voronoi多面体很大，可能会导致附近的多面体变得很小。因此，你可以尝试找到一些连接不同多面体体积的不等式。
许多研究人员尝试了这种方法，有些人甚至声称取得了成功，但没有任何一种方法被广泛认可为确切的证明。
最终，这个问题由Thomas Hales及其合作者解决。他们采用了类似的基本策略，但加入了大量的技术性调整。
他们对Voronoi单元进行了更精细的改进，不仅简单测量体积，还创建了一个综合得分体系，结合了体积和其他多个小的临时调整。他们的目标是建立这些不同得分之间的线性不等式，以最终得出密度的上限，并希望达到最优密度。
这种方法非常灵活，但也因为可选择的方案过多而显得复杂。
Thomas Hales和他的学生Samuel Ferguson发现，每当他们在解决最小化问题时遇到困难时，都可以通过调整评分函数来避开这些问题。然而，这使得评分函数变得越来越复杂，每次更改都可能需要大量时间。
更糟糕的是，这种新函数与之前论文的内容有轻微的不兼容，这就需要重新修改之前的论文。
最初，他们并未打算依赖计算机，但随着项目的复杂度增加，他们不得不更多地依靠计算机进行处理。到1998年，他们最终宣布项目成功，通过线性规划计算，从一个包含150个变量的优化问题中得出了开普勒猜想的证明。
该证明包含了250页的手稿以及3GB的计算机程序、数据和结果。
在审核过程中，这个证明遇到了重大困难。它被提交给了几家顶尖的数学期刊，评审过程历时四年，并由一个专家小组负责。
评审结束后，他们表示对证明的正确性有99%的信心，但无法确认计算机计算的准确性。他们采取了一种不同寻常的做法，在发表论文时加了一个注释说明这一点，但后来又撤销了这个注释。
当时，是否接受计算机辅助证明作为正式证明存在很大争议。尽管我们现在对此更有信心，但在论文发表后，仍有人对其是否真正构成证明持有疑虑。
因此，这可能是首个真正需要将问题完全形式化的高知名度案例。为了实现这一点，Hales 发起了一个名为 Flyspeck 的项目。
他最初估计需要20年才能完成证明的形式化工作，但实际上，在21位合作者的帮助下，只用了12年就完成了。这一成果最终于2014年公布。
因此，我们现在对这一结果充满信心。
我们已经开始探索更高效的工作流程来进行形式化，尽管这一过程仍然繁琐，但正在逐步改进。
Peter Scholze 是一位非常杰出的年轻数学家，因其众多成就而闻名，特别是他创立了一个名为“浓缩数学”的新数学领域。
该领域运用代数、范畴论及其他代数工具来解决那些传统上难以用代数方法处理的泛函分析和函数空间理论问题。Scholze建立了一整套范畴，其中包括所谓的浓缩阿贝尔群和向量空间。他的核心观点是，我们在研究生课程中学到的所有关于函数空间的分类都不够精确或不够自然，而他提出的分类方法具有更好的性质。
然而，他还需证明一个至关重要的消失定理。该定理的证明涉及某些范畴论群的技术性计算，从而成为其理论的基础。
他在一篇博客文章中讨论了这一成果，并提到他花了整整一年的时间专注于证明该定理，几乎到了痴迷的程度。最终，他们将论证过程记录下来，但由于无人敢深入检查这些细节，他心中仍存有疑虑。
有了这个定理，浓缩公式在泛函分析中的应用才能得以实现。由于其基础性和重要性，99.9% 的确定性还不够充分。
全球各地有许多研究浓缩数学的工作组，但都未能完成此定理的证明。尽管这一证明过程并不吸引人，但他认为这可能是自己最重要的成就之一，前提是必须确保其正确性。
后来，他们采用了一种更为现代的语言——Lean。
Lean 是一种近年来发展起来的语言，它是一个众包项目，旨在构建一个庞大的数学库。与从数学基本公理出发推导一切不同，该库已证明了许多中间结果，例如本科数学课程中常见的基础群论、拓扑学等主题，并将其形式化。
为了形式化这一理论，他们不得不增加许多额外内容。尽管数学库尚未完善，仍有诸如同调代数、层理论等领域需要加入，但在短短18个月内，他们成功地形式化了这一定理。
证明基本正确，尽管存在一些小的技术问题，但未发现重大错误。他们找到了一些简化的技巧，由于某些技术步骤过于复杂而难以形式化，因此不得不寻求一些捷径。
实际上，这个项目的价值更多体现在间接方面。
首先，他们极大地丰富了 Lean 数学库。现在，该数学库能够处理大量抽象代数，其能力远超以往。此外，还开发了其他支持软件，如“蓝图”（blueprint）。
直接形式化一个庞大的证明，比如长达 50 页的证明，是非常痛苦的过程，因为你必须将整个证明牢记于心。
正确的做法是，先将一个大证明分解成数百个小步骤，并编写一个“蓝图”。每一步都可以独立形式化，然后再将所有步骤组合起来。团队中的不同成员可以在各自负责的步骤中进行形式化工作。
此外，这个项目的另一项成果是，我们现在拥有了一份数万行代码的形式化证明。目前正努力将其转换为人类可读的格式。此外，还开发了一些工具，可以将用 Lean 语言编写的证明转换成人类可读的形式。
例如，这里有一个拓扑问题的证明，已经被成功转换为人类可以理解的格式。
因此，这些文本都是从形式化证明中由计算机自动生成的，看起来就像人类编写的证明一样，使用了相同的数学语言，但具有更高的交互性。
你可以点击任何位置，系统会显示当前的假设、你正试图证明的内容以及相关的变量。如果某个步骤过于简略，你可以展开查看其来源，并深入探究至所需的公理。我认为这是一个极好的创新，我相信未来的教科书将会采用这种互动的形式，首先进行形式化处理，然后提供比现有教科书更具互动性的版本。
受此启发，我也开始了我的形式化项目。
去年，我和包括Tim Gowers在内的一些人共同解决了一个组合学问题。这个问题涉及具有“小倍增”特性的二进制Hamming立方体的一个子集，该子集的大小受到一定限制。
我们很快完成了形式化工作，证明大约有33页长。
事实上，这可能是迄今为止最快完成形式化的实际研究论文，由约20人的团队在三周内完成，利用了Scholze项目中开发的所有这些蓝图。
这使得证明过程更加开放和协作，同时还能获得精美的可视化效果。
正如我所说，你需要做的第一件事是将大定理拆分成许多小部分。我们得到的定理被称为PFR，对应于图表底部的一个小圆圈。
然后我们引入了其他所有证明，PFR证明需要依赖于几个先前的证明。
因此，存在一个依赖图，颜色表示是否已经形式化。绿色圆圈表示已经形式化的证明，蓝色圆圈表示尚未形式化但已经准备就绪（例如，所有定义都已经到位）。白色圆圈表示尚未形式化，需要有人来编写。
这样，你就得到了一个任务树，这个项目的美妙之处在于可以让所有人在这个图的不同部分上独立协作。
参与者中有些人甚至不是数学家，而是计算机程序员，但他们非常擅长解决这类小拼图式的问题。每个人选择了一个自己能够处理的圆圈，最终在三周内完成了整个项目，这是一个非常激动人心的过程。你知道，在数学领域，我们通常不会与这么多人合作，我见过的最多也就五个人。这是因为当你在一个大项目上合作时，必须信任每个人的数学都正确，超过一定人数就变得难以管理。
然而，在这样一个项目中，Lean 编译器会自动检查，你无法上传任何无法编译的内容，因此可以与素未谋面的人合作。
这是一个例子，我认为这将成为未来数学研究的一种越来越普遍的方式。尽管工具正在改进并变得更加用户友好，但仍然需要一定的编程专业知识。
另一方面，如果你需要修改证明中的某个数字，例如，某个定理中原本有一个12，后来要将其改为11，从而得到一个稍微更强的定理。通常情况下，如果这样做，你需要重写整个证明，或者尝试将12替换为11，但还需要检查是否引入了其他错误。
然而，当我们将这一过程形式化后，只用了几天时间就把12改成了11。我们只需在一处将12改为11，然后 Lean 在大约五个地方报错。
目前有许多大型证明形式化项目正在进行中，其中最大的可能是 Kevin Buzzard 的项目，他刚刚获得了大量资金，用于在 Lean 中形式化费马大定理。他表示这个项目的关键部分将需要五年时间才能完成，但他并未声称五年内能完成全部，这非常有趣。
这就是形式化证明助手的一个应用。
接下来我将谈谈机器学习。
机器学习利用神经网络来预测各种问题的答案，这些答案在众多领域中都有广泛的应用。然而，在这里，我将不讨论使用神经网络来猜测偏微分方程解的方法。
我想谈谈的是机器学习在结理论中的应用。
结理论是数学中一个非常有趣的领域，它融合了多种不同的数学分支。
结是指空间中封闭的一圈绳子或曲线。如果可以通过连续变形将一个结变成另一个结，并且在此过程中绳子不能自相交，则认为这两个结是等价的。
（图源：维基百科）
因此，结理论中的一个基本问题是：两个结何时是等价的？即，是否存在一种方法可以将一个结转变成另一个结？
通常解决这个问题的方法是开发所谓的结不变量。
这些不变量可以是各种数值，有时也包括多项式，你可以将这些数值或多项式附加到一个结上，无论你如何连续变形这个结，这些数值都不会改变。因此，如果两个结有不同的不变量，那么它们就不可能是等价的。
有许多不同类型的结不变量。例如，有一种叫做“签名”的不变量，你可以通过平展结并计算交叉点（无论交叉是向上还是向下）来创建一个特定的矩阵。还有一些著名的多项式，如琼斯多项式和亚历山大多项式，这些多项式与许多数学领域有关联。
另一种不变量是所谓的双曲不变量，来源于几何学。
你可以取结的补空间，这通常被称为双曲空间，它具有一系列的几何结构和距离概念。你可以保留它的体积和其他一些不变量。因此，这些不变量是实数或复数，每个结都带有一些组合不变量，如签名、双曲几何不变量等。
这里有一系列带有各种双曲变量的结，有些被称为双曲体积等。
尽管已知存在两种不同的方法来生成关于结的统计数据，但之前没有人能发现这两种方法之间的任何联系或共同点。
直到最近，人们开始尝试使用机器学习来解决这个问题。他们创建了一个包含数百万个结的数据库，并在这个数据库上训练了一个神经网络。结果发现，训练后的神经网络能够利用所有双曲几何不变量，并且在大约90%的情况下能够正确预测签名。
因此，他们创建了一个黑盒子，这个黑盒子能够告诉你签名以某种方式隐藏在这些几何变量中，但并不揭示具体是如何做到的。尽管如此，这个黑盒子仍然很有用，因为一旦你拥有它，就可以随意使用它来进行预测。
接下来，他们进行了一种非常简单的显著性分析。这个黑盒子接收大约20种不同的输入，其中包括你的变量类型，并输出一个结果，即签名。
他们发现，在这20个输入中，只有三个实际上对输出起到了重要作用，包括纵向平移以及子午线平移的实部和虚部。
一旦确定了哪些变量最重要，他们可以直接将签名与这三个特定输入进行比较，然后由人类进行判断。
通过观察这些图表，他们提出了一项猜想，结果却是错误的。他们实际上又使用神经网络来证明这个猜想是错误的。
通过这次失败，他们提出了一个修正版本，这是一个正确的命题，解释了这一现象。因此，他们现在拥有一个理论解释，阐述了为什么签名与这些特定的统计数据如此密切相关。
我认为这反映了机器学习在数学领域应用的日益增长的趋势。尽管机器学习本身无法直接解决数学问题，但它能够提供大量有价值的线索，揭示数据之间的潜在联系，并为研究指明方向，而建立这些联系的工作仍需要人类来完成。最后，我们还有大型语言模型，这些模型可能是最引人注目的，也可能最具新闻价值。你知道，神经网络已经存在了20多年，而语言模型大约存在了5年左右，但直到最近，它们才达到了接近人类水平的输出质量。
你们可能都听说过GPT-4。在其发布时，一篇非常著名的论文详细描述了它的能力，并且它确实展示了这些能力。
这是一个来自2022年国际数学奥林匹克（IMO）的简化版问题，针对这个问题，系统给出了一个完整且正确的解决方案。
然而，这是一个精心挑选的例子。他们在测试数百个IMO级别的问题时，成功率大约只有1%。这意味着它们能够解决特定问题，但前提是问题必须以正确的方式进行格式化。即便如此，这仍然是一个非常了不起的成就。
另一方面，这些工具的一个有趣之处在于，人类觉得困难的事情，AI有时可以轻松完成，而人类觉得简单的事情，AI却常常表现得很差。这是一种非常正交的解决问题方式。
在另一篇论文中，他们要求模型进行一个基本的算术计算“7×4+8×8”。模型给出的答案是120，但在逐步解释过程中，又得出了92的答案。这表明，虽然AI有时能找到正确答案，但其处理过程并不总是准确无误。
因此，人们正在尝试各种方法，将这些模型与更可靠的软件结合起来，这样就不需要自己进行计算，而是可以将计算任务交给Python等工具来完成。
你还可以强制要求模型仅生成正确的答案，并且只使用一种证明助手的语言进行输出。如果输出无法编译，可以将其退回到AI系统，迫使AI重新尝试。此外，你也可以直接教授它解决国际数学奥林匹克（IMO）题目的一些技巧，例如尝试简单的情况或采用矛盾法证明。
人们正在尝试各种方法来改进这一过程，尽管目前还无法解决大多数数学问题，更不用说复杂的数学研究问题，但进展正在逐步显现。
除了直接解决问题之外，这些模型还可以作为灵感的源泉。我自己也尝试过这些模型，处理了多种不同的问题。
有一次，GPT-4为我提供了10种解决问题的方法，其中5种显然无效，但我发现了一种之前未曾注意的技术——生成特定问题相关的函数。我意识到这是一种正确的方法。因此，在某种程度上，这些模型确实有用，虽然还不完美，但也并非毫无价值。
另外，还有一种AI辅助工具对证明助手特别有用。
如前所述，编写形式化的证明是一项非常繁琐的任务，就像编写计算机程序一样，必须确保语法完全正确。如果漏掉任何一个步骤，整个证明就无法编译。
我使用了一款名为GitHub Copilot的工具。当你写下部分证明时，它可以尝试预测下一行的内容。大约20%的情况下，它的预测是准确的，你可以接受这些预测并继续编写。
在这个例子中，我试图证明一个命题，灰色的行是Copilot建议的内容。结果显示，第一行的建议没有用处，但第二行则非常有用。因此，你不能盲目接受所有建议，因为它们不一定能够顺利编译。
然而，如果你对代码的工作原理已有大致了解，这将大大节省你的时间。
现在还有一些实验尝试让AI提出一个证明方案，然后将其提交给编译器。如果出现编译错误，再将错误信息反馈给AI系统。
我们已经开始尝试证明，那些只有四五行的内容可以通过这种方法得到约束。当然，对于数以千计行的大型证明，要立刻实现形式化还遥不可及，但这种方法已经成为了有用的工具。那么，我们现在处于哪个阶段呢？
有些人希望在未来几年内，我们能够直接使用计算机解决数学问题，但我认为这个目标还很遥远。
对于非常具体的问题，你可以设计专门的AI来处理其中的一部分。但即便如此，它们也并非完全可靠。虽然这些AI可能有用，但依然存在局限性。
至少在未来几年里，AI 主要仍将是辅助工具，不仅限于我们熟悉的暴力计算辅助，人们正在尝试各种创新的方法，希望AI能够擅长生成有见地的猜想。
我认为这是一个特别令人兴奋的方向。
我们已经看到一些关于结的小例子，AI 已经能够猜测出两种不同统计数据之间的关系。因此，只需创建这些庞大的数据集并将其输入到AI中，它们就能自动生成不同数学对象之间许多有价值的关系。
我们目前还没有掌握如何做到这一点，部分原因是缺乏这些大型数据集，但我认为这是有可能实现的。
证明定理是一个既痛苦又耗时的过程，我们通常一次只能证明一个定理，即使效率很高，也可能只是一次证明两三个。但借助AI，你可以想象将来不仅仅解决一个问题，而是同时处理一类包含1000个问题的情况，然后对AI说：“好，我希望你用这种技术来解决这1000个问题。”
使用这种技术，我能解决多少问题？如果结合多种方法，我能达到什么效果？你可以开始探索问题的空间，而不仅仅是逐一解决每个问题。
这是一个需要几十年时间，通过成百上千篇论文逐步摸索各种技术能做什么、不能做什么的过程。
但有了这些工具，你真的可以以前所未有的规模进行数学研究。
因此，未来将非常令人期待。我的意思是，我们仍然会以传统方式证明定理。事实上，我们必须这样做，因为如果我们自己不懂如何操作，就无法指导这些AI。但我们将能够做许多现在无法做到的事情。
参考链接： [1] https://www.youtube.com/watch?v=e049IoFBnLA [2] https://www.reddit.com/r/singularity/comments/1f0o9vo/terence_tao_says_ai_could_solve_mathematical/
网友：需要一段时间来消化
用于解决数学难题
"AI工具像是概率函数"
论文只有6页纸
还是个“意外”收获（doge）
