富兴配资一位菲尔兹奖得主，成为数学领域人工智能的布道者

借助自动化证明检查器，一个难题可以被分解成小块，逐块解决，然后重新组合，并确信每一部分都是正确的。对一些人而言，这预示着数学研究的一个新领域。

撰文｜Kevin Hartnett

编译｜數學家编译小组

诸如 Lean 之类的自动化证明检查器可以提供铁一般的保证，确保数学证明是有效的。丨图源：Samuel Velasco/Quanta Magazine

陶哲轩从不畏惧非传统的想法。2014 年 11 月，他与另外四位杰出数学家一同出席了一个专家小组讨论会，他们都是首届突破奖数学奖的获得者，该奖项附带 300 万美元的奖金。这些获奖者的谈话内容广泛，从数学是被发明的还是被发现的——大多数数学家都同意，至少从感觉上像是一种发现行为——到评估我们生活在数字模拟中的可能性。“是啊，我觉得我们其实不是真实的，”Maxim Kontsevich 说，他在 20 世纪 90 年代于数学和物理学的交叉领域做出了自己最重要的研究。

然而，在 40 分钟的讨论过程中，最令人难以置信的言论来自陶哲轩。他预测，在未来，数学家们可能不再独自或与两三个人的小团队合作，而是可能同时与数百名其他人一起参与项目。他还以他谦逊、低调的方式说，当这些合作结束时，其结果可能不是由人类审稿人，而是由计算机来检验。“有朝一日，我们可能不再用 LaTeX 写论文，而是用某种能由智能软件转换为形式语言的编程语言来写，每当你写错时，你会得到一个编译错误——计算机不明白你是如何推导出这一步的，”他说。

The Proof in the Code 探索了人类与计算机数学协作的时代。丨图源：Samuel Velasco/Quanta Magazine

这番言论让活动主持人和其他获奖数学家都觉得荒谬至极，以至于相比之下，活在模拟世界的假说反而显得合理了。比起数百位数学家一起工作这个想法本身，更令人惊讶的是这种合作会吸引陶哲轩——因为如果说世界上有谁似乎特别适合单干的话，那就是他了。

陶哲轩 1975 年出生于澳大利亚的阿德莱德，他的父母在三年前从香港移民到这个国家。很早时候，他们的长子就显露出了与众不同的迹象。陶哲轩两岁时，家人带他去朋友家做客，结果发现他和几个六岁的孩子聚在一起，正在用木块演示如何数数。当被问及如何学会数东西时，他回答说是在《芝麻街》（Sesame Street）上看到的。五年后，陶哲轩七岁时，他开始学习微积分。

1985 年春天，陶哲轩的父母带他来到美国，为期三周，期间他见到了当时在 Johns Hopkins 大学的“数学早慧少年研究”项目负责人 Julian Stanley。Stanley 称陶哲轩拥有他见过的“最出色的数学能力”。同年，陶哲轩还结识了著名数学家 Paul Erdős，他当时正在阿德莱德访问。有一张著名的照片，当时 Erdős 正在阅读膝上的一份文件，而年仅10岁、有着浓密黑发的陶哲轩则专注地看着，手指若有所思地举到下巴边。Erdős 当时72岁，就像陶哲轩的爷爷。

陶哲轩的少年传奇在1986年他参加国际数学奥林匹克竞赛（IMO）时进一步增长。他在第一次参加就获得了铜牌，成为有史以来达到这一成绩的最年轻参赛者，时年 10 岁。在接下来的两年里，他先后成为最年轻的银牌得主，并最终成为最年轻的 IMO 金牌得主。他的正规教育也以同样以加速的节奏进行。他 15 岁时从阿德莱德当地的 Flinders University 毕业，并于1992年秋天与父亲一起登上飞往新泽西州的飞机，开始了他在 Princeton University 的数学博士生涯。Erdős 曾支持陶哲轩提前进入该项目，并在推荐信中写道：“我相信他将会成长为一位一流的数学家，或许是一位真正伟大的数学家。”

当时72岁的 Paul Erdős 与10岁的陶哲轩在一起。丨图源：Billy Grace Tao 供图

Erdős 说得没错。到陶哲轩24岁时，他已经做出了足够多的新发现，可以自主选择终身教职岗位；他最终决定在 University of California, Los Angeles 安顿下来。大约在那时，他遇到了一位名叫 Ben Green 的年轻英国数论学家。两人开始合作证明：在大量质数集合中，必然会以某种方式出现某些模式，即算术级数（集合中的数字按固定间隔递增，例如 7，10，13，16），尽管质数看似随机地分布在数轴上。他们的证明成为陶哲轩早期职业生涯的标志性成果，为他赢得了 2006 年的菲尔兹奖，并将他推向了数学界的顶端。

陶哲轩本可以不与任何人合作就建立起成功的职业生涯，但他不喜欢那种工作方式。他将与其他研究者合作视为发现新思想的主要途径——把你所知道的和我所知道的结合起来，看看会发生什么。

这种方法使得陶哲轩的数学研究涵盖了异常广泛的主题，从解析数论（包括关于质数的 Green-Tao 定理），到分析学（他研究了描述流体行为的 Navier-Stokes 方程的性质），再到根据数字数据构建 MRI 图像的算法（这项 MRI 合作是在陶哲轩与当时在 California Institute of Technology 的统计学家 Emmanuel Candès 各自送孩子去幼儿园的谈话中发展起来的）。这种对合作探索新知的渴望也促使陶哲轩在公共平台上进行了大量工作。2007年，他开通了一个博客，开始定期发布关于自己研究的最新动态。到那时，陶哲轩不仅是他所在的领域，更是世界上最著名的数学家之一。他的博文受到了很多关注，有时会在评论区引发长时间的讨论，陶哲轩也会热情地参与其中。他这样做是因为他觉得这很有趣，同时也希望这些对话能产生新的想法。

大约在同一时间，另一位早期的数学博主也有类似的想法。与陶哲轩一样，Timothy Gowers 也是一位杰出的研究型数学家，喜欢公开交流。不过， Gowers 并不将希望寄托于博客评论区偶然出现的机会，而是希望以一种有组织的方式引导公众的活力。2009 年 1 月，他发表了一篇博文，宣布他希望能促成一种新型的“大规模协作数学”。他会在一个开放的在线论坛上提出一个问题，“任何对此问题有见解的人都可以参与进来”。他将其命名为 Polymath Project。

陶哲轩立即加入了进来。和 Gowers 一样，他知道有些数学问题比其他问题更适合通过大规模协作来解决。关键在于，正如陶哲轩在 Gowers 初始博文的评论中所写，要找到那些能够“产生大量更简单的子问题……而这些子问题很大程度上可以并行处理”的问题。通过将大问题分解成独立的部分，不同的团队或个人就可以独立工作，然后将各自的成果作为整体的一部分进行整合。同时，陶哲轩也明白，Polymath 模式可能面临的最大挑战在于组织：协调大家的贡献，并检查确保所有贡献都是正确的。

对于第一个 Polymath 项目，Gowers 提出了改进一个名为 Hales-Jewett 定理的结果，该定理涉及用两种不同颜色中的一种对网格中的单元格进行着色，会出现什么模式。经过几个月的工作，通过数十位数学家的数千条评论进行协调，该小组证明了一个更精确的陈述——关于这些着色模式是如何出现的。那年秋天，他们以“D. H. J. Polymath”这个化名发表了这项成果，成为了一篇史无前例的数学论文。Gowers 的实验成功了。它让许多数学家（无论是专业人士还是业余爱好者）能够共同工作，并最终产生了一个证明。

在接下来的十年里，又陆续开展了 15 个 Polymath 项目，其中一些由陶哲轩领导，该计划也引起了主流媒体关注。2011 年 10 月 29 日，The Wall Street Journal 刊登了一篇题为“The New Einsteins Will Be Scientists Who Share”的文章，报道称 Polymath Project“开创了解决问题的新方法”。

一张解释证明辅助工具结构的图示（不知为何，章鱼表情符号成了 Lean 社区里表达开心的御用符号)。Samuel Velasco丨图源：Samuel Velasco/Quanta Magazine

不过从在其他方面看，Polymath Project 其实是一个超前于时代的理念。陶哲轩置身于数学活动热潮的中心，这令他兴奋不已，但他也认识到博客的评论区作为一个协作平台是有限的。大规模开放协作增加了某种偶然发现的可能性，但同时也提高了参与者犯错的风险。防范错误的唯一方法是让协调员（版主）仔细检查所有的工作。但这种审核协调机制破坏了 Polymath 的愿景。

陶哲轩真正追求的是一种高效的、新型的科学发现形式。过了一段时间，他开始意识到 Polymath 模式并非如此。他认为，要实现这一目标，需要某种计算机验证——一种自动检查成果的方法，而不是手工检查。但鉴于 2010 年代的技术水平，他这个愿望就像有载客飞船去火星一样遥不可及。

陶哲轩了解计算机验证数学已有多年。他知道一些成功的案例，但也知道形式化数学在当时仍然不切实际，所需付出的努力远超其带来的价值，在大多数情况下得不偿失。尽管如此，陶哲轩仍对其潜力很感兴趣。在世界顶尖数学家中，他几乎是唯一一个看到了数学新方法潜力的人。

2022 年 7 月，部分出于好奇，他组织了一个研讨会，探讨计算机辅助数学研究的各种不同方式。他发起了一个联合组织者团队，其中包括 Kevin Buzzard，他当时是世界上最引人注目的形式化数学布道者。

在会议召开前夕，陶哲轩认为 Lean（一种允许数学证明像计算机代码一样编写和检查的软件）是一个复杂的程序，需要数月时间学习。Buzzard 说服他尝试一下。在这样的鼓励下，陶哲轩感到了一种强烈的责任感，要以身作则——如果要继续推广机器辅助证明，必须先从自己开始尝试。

2023 年 10 月 9 日，陶哲轩在社交媒体上发帖：“我最终决定要熟悉一下 #Lean4 交互式证明系统（必要时会借助人工智能辅助来帮助我使用它）。”

在 MathOverflow（一个颇受数学家欢迎的在线论坛）上，陶哲轩发现了一个关于 Maclaurin 不等式的问题。他决定回答这个问题，作为形式化的一次实验。首先，他像写普通数学论文一样写出了证明，很短，只有10页。然后他把注意力转向了他真正的目标：看看能否用 Lean 将这个简单的证明形式化。

起初，陶哲轩认为他可能在一周内完成，但他很快就直面用手写数学公式和用 Lean 输入数学之间的差异。陶哲轩观察到，证明中困难的部分在 Lean 中很容易形式化，而简单的部分却需要惊人的工作量。

在普通论文中，陶哲轩无需特意说明：如果你有三个数字，每个都大于1 ，那么它们的和必然至少是 3。但 Lean 不能直接接受这样的断言，陶哲轩不得不花时间在 Mathlib（一个已经形式化数学的数字库，Lean 用户在编写证明时会用到它）中寻找一个引理来证明这个不言自明的关系。类似地，在非形式化数学中，并不总是需要指定你使用的是哪个数系。例如，数字3同时是一个整数、一个自然数和一个实数。在他最初的论文中，陶哲轩可以直接写“3”，而不必指明他脑中所想的是哪种3。然而，在 Lean 中，他必须明确说明。陶哲轩发现他的证明一直无法编译成功，因为他在形式化时的不同步骤里忽略了指定正确的类型。直到将近一个月后的 11 月 6 日，陶哲轩才在他的博客评论中写道：“只是提一下，我已经成功地将这篇论文的结果在 Lean4 中形式化了。”结果微不足道，他用来形式化它的 Lean 代码也很糟糕。尽管如此，陶哲轩现在正式成为了 Lean 社区有贡献的成员。

在学习 Lean 的同时，陶哲轩还在继续从事许多其他研究项目。其中包括一个与他长期合作者 Ben Green、Timothy Gowers 以及 Freddie Manners（Green 以前的学生，现为 University of California, San Diego 教授）合作的项目。这是一个精英合作团队——Gowers 和陶哲轩一样，曾获得菲尔兹奖，而 Green 是该领域最有成就的数论学家之一。

这个团队瞄准了一个特定的问题，该问题围绕着一个称为“和集”（sumset）的数学对象展开。如果你有一组数，可以用它来形成另一个相关的集合：它的和集。和集是通过取第一个集合中每一对不同的数之和构成的。所有这些和共同构成了原始集合的和集。

如果原始集合的数都是随机的，那么它的和集会相对较大。一个有 10个随机数的集合，其和集大约有50个数；一个有1000个数的集合，其和集大约有500,000个数。但是，如果原始集合不是包含随机数，而是遵循某种模式，那么它的和集会小得多，因为许多和会多次出现，并且每个和在和集中只计入一次。数字1到10的集合就是一个例子——它的和集只包含17个数（而不是像10个随机数集合那样预期的50个），因为许多和会重复1+6，2+5，3+4和都等于7，并且在和集中只计入7一次。

除了具有小的和集之外，数字 1到10 也是一个算术级数的例子，因为它们按恒定间隔递增。20 世纪 60 年代，计算机科学家 Katalin Marton 提出一个猜想，并认为这并非巧合。她预测，产生小和集的集合也必然包含长的算术级数。Gowers、Green 和陶哲轩在21世纪初对一个该问题的精细化版本——Freiman-Ruzsa 多项式猜想取得了进展，但最终还是卡住了。2023年，陶哲轩、Green 和 Manners 再次拾起这个问题，打算引入 Manner 发展的概率论技术。

他们意识到，将这些技术与 Gowers 早期的想法结合起来，或许能解决整个问题。他们邀请 Gowers 加入合作，这个四人组在 2023 年夏天取得了稳步进展。到了深秋，他们成功了。11 月 9 日——就在陶哲轩将他第一个正式的 Lean 证明上传到 GitHub 的三天后——他们将证明上传到了 arxiv.org。

由于心中惦记着 Lean，陶哲轩向他的三位合著者建议，可以尝试将他们的论文形式化。这项工作似乎是一个很好的形式化候选，既因为它是一个重要的成果，也因为它依赖于相对简单的技术。他们不必花费数月向 Mathlib 添加先决材料——大多数必要的定义已经存在了。

然而，Green、Gowers 和 Manners 并不特别感兴趣花时间去学习 Lean。于是陶哲轩独自开始了——尽管他知道他可能不会独自一人很久。任何由他领导的项目都可能引起关注。

11 月 13 日，陶哲轩在一个专注于 Lean 的聊天群中开启了一个新频道。“大家好。我正在考虑启动一个项目，在 Lean4 中将 Timothy Gowers、Ben Green、Freddie Manners 和我本人最近对多项式 Freiman-Ruzsa（PFR）猜想的证明形式化，”他写道。他会利用这个频道来协调该项目的工作，并且“欢迎任何愿意帮忙的人以他们力所能及的方式为该项目做出贡献”。这是 Polymath Project 的重启，只不过这一次他们是在形式化一个已有的成果，而不是试图证明一个新的成果——而且所有的工作都将由 Lean 验证，这意味着陶哲轩不必亲自检查。

一天之内，Stockholm University 的博士生 Yaël Dillies 就为该项目建立了一个粗略的框架，将证明分成了 13 个部分。在每个部分中，陶哲轩确定了需要形式化的引理和定义的序列。在一篇典型的数学论文中，引理（有助于构建更大定理证明的更简单的成果）可能有大约20行，但对于 PFR 的形式化，陶哲轩将证明分解成了只有 5 行的引理。他的目标是使证明尽可能模块化，让更多人能够做出小的贡献。

在第一周，论坛上的大部分活动都是关于形式化概率论中的基本概念，这些概念是证明所需的，但 Mathlib 中还没有。特别是，他们必须形式化香农熵——对数据源（如一组数字）中不确定性或无序程度的度量。除了进行数学形式化的工作之外，陶哲轩和其他人还在第一周花费时间弄清楚如何协同工作。起初，大家的交流比较自由，陶哲轩发帖说明他认为需要做什么，其他人则提出关于如何做的想法，很大程度上就像 Polymath 项目在博客评论中展开的那样。

11 月 22 日，陶哲轩列出了22个待解决的引理，并写道：“如果你想申领这些引理中的一个或多个，请在此帖中回复。”回复纷至沓来：“我想申领均匀随机变量的熵 :)”，London School of Geometry and Number Theory 的博士生 Paul Lezeau 写道。“我打算尝试处理一般的纤维化恒等式，”UCLA 的博士生 Aaron Anderson 回复道。

通过口耳相传，越来越多的数学家加入了这项工作。到 11 月底，陶哲轩就像一位忙碌的志愿者协调员，自己很少再写 Lean 代码，而是专注于为他人找任务。11月28日，他写道：“鉴于在 PFR 项目接近完成时我们可能暂时有志愿者过剩的情况，我想到了一个额外的小任务，也许有人愿意做。”46分钟后，Kim Morrison 回复说他们已经完成了这项任务。“哇，真快！谢谢！”陶哲轩答道。

甚至在形式化完成之前，Lean 社区就开始讨论其意义。他们特别争论了该项目的效率是否预示着快速形式化的新时代，还是仅仅反映了陶哲轩的独特影响力。在小组帖子的总结发言中，陶哲轩反思道，他自己并没有编写太多代码。“这实际上让我很受鼓舞，因为它表明数学家们无需具备高超的 Lean 编程技能，就能牵头开展Lean形式化项目（当然，至少需要具备陈述引理的能力，即便无法证明它们）。”八分钟后，Utrecht University 的数学家、Mathlib 计划的负责人 Johan Commelin 回复道：“我不想马上抢占这个话题，”接着质疑了陶哲轩在项目中所学到的经验教训是否具有普遍适用性。“当然，由于该项目的高知名度，你得到了很多帮助，”他写道。

Commelin 还指出，尽管像 PFR 这样的项目参与起来很有趣且令人兴奋，但参与这些项目并不为年轻数学家申请学术职位时带来好处。“目前，尚不清楚形式化者（姑且这么称呼吧）将如何被数学界认可，以及这些活动在就业市场上将如何被评估。”陶哲轩回答：“不管怎样，我很乐意在推荐信中酌情提及对这个项目的贡献。”

到 2024 年，陶哲轩已成为最引人注目的、宣传机器辅助数学潜力的公众声音。他在拜登总统的科学技术顾问委员会任职已进入第三个年头，并成为了一个关于生成式人工智能的工作组的联合主席。在 2024 年的两场高知名度的演讲中，他表达了他对一种新型数学合作的愿景：这种合作结合了人类的洞察力、大型语言模型的创造力，以及形式化验证系统提供的正确性保证。

他之所以得出这个观点，部分原因是他看到了当前 AI 工具的明显局限性。它们擅长解决简单的问题或有大量先前数据的任务，但在数学的前沿——那里已发表成果很少，可用于训练的数据也很少——AI 就力不从心了。在他早期使用大语言模型的实验中，他观察到它们表现得像过于自信的本科生：它们会提出各种建议，但却没有足够的能力来判断这些建议的好坏。

不过，陶哲轩心中已有前进的方向。他认为 AI 不会很快取代人类数学家，但他确实认为 AI 特别适合帮助解决某些类型的复杂数学问题：那些可以分解为成千上万个易处理的小型子问题的问题——基本上与适合 Polymath 项目的是同一类问题。在这种规模上，数学家可以使用 AI 来解决大量最简单的子问题，将其结果输出为 Lean 可以检查的形式化证明，然后再介入处理剩余的、最困难的、需要他们自己解决的问题。2024 年，陶哲轩向任何愿意倾听的人宣传这一愿景，并且在 PFR 项目之后，他意识到如果他真的相信这项工作，他需要挺身而出，亲自领导。他也立刻确定了首先从哪个问题开始。

这是一年前他偶然发现的一个问题。2023 年 7 月，一位 MathOverflow 用户提出了一个看似简单的谜题。考虑一个像加法这样的运算，它可能遵循某些基本的代数定律，如交换

在许多情况下，一个定律与另一个定律之间没有关系——例如，交换律并不意味着结合律。

这个 MathOverflow 上的问题涉及两个特定定律之间的关系，另一位用户迅速回答了它。

但是，关于定律之间如何普遍关联的问题引起了陶哲轩的好奇心。他没有一个接一个地解决谜题，而是开始绘制一个粗略的图表，展示不同可能的代数定律之间如何相互关联。很明显，这幅图景可能非常复杂。

他发现，如果他将研究限制在涉及恰好四次运算的代数法则上，那么需要考虑大约 4,694个定律。每个定律可能蕴含或不蕴含任何其他定律，从而产生了 2200万个逻辑蕴含关系需要检查。一旦他检查了所有关系——要么证明它们成立，要么找到它们不成立的反例——他就能够全面了解这全部 4,694个定律之间是如何相互关联的。他认为，这样的规模正好适合他所提出的这种新数学方式。

陶哲轩将他的新事业称为“Equational Theories”，并于 2024 年 9 月 25 日在他的个人博客上发帖宣布了该项目的启动。他开篇逐一列举了过去大规模公共数学合作之所以困难的主要原因，然后写道：“像 Lean 这样的证明辅助语言，提供了一种克服这些障碍的潜在方法。”

起初，陶哲轩和越来越多的加入他的志愿者针对被称为“原群”（magmas）的简单数学结构测试了,4,000多个定律。原群是一种简化版本的算术系统，可以作为一个有用的起点，因为任何对原群不成立的定律都不可能蕴含其他更复杂的定律。参与者们迅速使用基本的 Python 脚本测试了数百万个这样的简化系统，并在几天内解决了这2200 万个潜在蕴含关系中的 99%以上。陶哲轩在第二天（9月27日）发帖称，他对项目进展之快感到惊讶：“这个项目的进展速度远远快于我的预期，其规模扩大的速度也远远超过我的预期——仅仅48小时，很大一部分蕴含关系很可能很快就能解决！我以为为期三周的 PFR 项目已经很快了，但这个速度简直疯狂得离谱。”

一旦最简单的蕴含关系得到解决，“Equational Theories”的志愿者们以去中心化的方式转向了自动化定理证明器，这些证明器可以在无需交互式帮助的情况下自行搜索问题的解决方案。这些证明器，加上传统的人类聪明才智，逐个攻克了悬而未决的问题。

就像一位科学家看着自己的造物变为现实，陶哲轩欣赏着工作的展开。“这个项目似乎正在成功地实现去中心化；特别是，现在有很多活动是我并不完全了解的，”他写道。

对许多数学家来说，陶哲轩的项目很有趣，但也很奇怪。Buzzard 关注着这个项目，被这个社会实验所吸引，但对“Equational Theories”的数学内容感到无聊。他认为它既基础又古怪，不过他还是钦佩陶哲轩的创造力。另一位著名数学家 John Baez 则更直言不讳。他说：“在我看来，这似乎是在巨大地浪费时间，”接着他承认他对大学橄榄球也有同感，而且很多人也喜欢那个。

一个月内，“Equational Theories”小组将 2200万个问题缩小到238 个。到 11 月下旬，减少到138 个。当他们逐步解决剩余案例时，进展放缓了。新年伊始，大约有 30个蕴含关系仍未解决，进展速度进一步放缓。到 3 月底，他们已在仅存的四个问题上卡了好几周。参与者们尝试处理剩余的问题，但由于只剩下这么少的蕴含关系，许多人逐渐离开了；陶哲轩的更新也从近乎每日的频率减少到每几周一次。

然而，解决全部2200 万个蕴含关系中的每一个从来就不是“Equational Theories”的真正目标。出于纯粹的好奇心，陶哲轩想要一张完整图景的地图，而现在他有了，尽管缺少了一些细节。更重要的是，他将“Equational Theories”视为一种根本性的数学新方式的试点项目——在这方面，它是不折不扣的成功。

在陶哲轩看来，“Equational Theories”是他希望成为“实验”数学新时代的开端。他心中所想的是那种已经发生在物理学等领域的变革。物理学曾经在很大程度上是一门理论学科，孤独的思想家或小型合作团队一次处理一两个问题——换句话说，它过去看起来很像数学现在的样子。但随着技术的进步，该领域出现了一个新的实验分支——在像 CERN 的大型强子对撞机这样的实验室里进行的大规模合作，数百甚至数千名具有专业技能的研究人员共同工作，并生成大量数据。这些实验并没有取代理论，而是对其进行了补充，新的研究成果在两种研究范式间双向流动、相互促进。

陶哲轩想象着数学界发生类似的演变。他相信，新颖的探究形式将不可避免地带来新颖的见解，正如过去一贯如此。当“Equational Theories”团队有条不紊地从他们庞大的表格中划掉蕴含关系时，他们偶然发现了真正新颖的数学构造——比如“原群上同调”，这是对群上同调概念的一种奇特扩展。群上同调是一个深刻且被广泛研究的领域，描述了群何时可以或不可以以某种方式被扩展。陶哲轩联系了 John Baez——这位“Equational Theories”的反对者同时也是上同调专家——询问这种构造以前是否见过。Baez 承认他从未遇到过。

在陶哲轩看来，这正是关键所在。该项目表明，数学可以以不同的、实验性的方式进行——并且在此过程中，它确实发现了一些真正新颖的东西。陶哲轩从未期望“Equational Theories”能挖掘出什么惊天动地的启示；他想要的是证明一种新型数学机器的有效性。从这个意义上说，它成功了。陶哲轩找到了一种做数学的新方法，而且他没有表现出任何要回头的意思。

本文原载微信公众号“数学家”（校对：慧玲；责编：），原标题：数学领域人工智能的布道者，有修订。