内容来源：https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

内容总结：

数学天才陶哲轩：从反叛者到AI数学布道者

21世纪初，当大多数数学家还在坚持传统研究方式时，菲尔兹奖得主陶哲轩就预言未来数学研究将发生颠覆性变革。如今，他正通过亲身实践，引领一场借助人工智能（AI）和计算机验证的数学革命。

作为当今世界最著名的数学家之一，陶哲轩从小便展现出非凡天赋：2岁用积木计数，7岁学习微积分，10岁获国际数学奥林匹克铜牌，24岁成为加州大学洛杉矶分校教授。2006年，因与合作者格林共同证明素数中存在任意长等差数列（格林-陶定理），他获得数学界最高荣誉菲尔兹奖。

早在2014年，陶哲轩就在一次颁奖典礼上提出惊人预言：未来数学家将不再独自研究，而是与数百人协作攻关；论文验证者不再是人类评审，而是计算机。这番言论当时被在场同行视为比“人类生活在数字模拟中”更荒谬的假设。

然而十年后，陶哲轩正以实际行动将这些预言变为现实。2023年，他学习并推广Lean4交互式证明系统。这是一种能将数学证明转化为计算机代码并自动验证其正确性的软件。他用一个月时间完成了自己的首个Lean证明，尽管过程充满挑战——计算机要求每一步推导都必须精确无误，甚至连“数字3”都要指明是整数、自然数还是实数。

同年11月，陶哲轩与三位顶尖数学家共同完成了多项式弗里曼-鲁兹猜想的证明。随后，他发起Lean形式化项目，将长达数十页的论文拆解成13个部分、数百个微型引理，邀请全球志愿者协同工作。与传统学术合作不同，所有贡献通过Lean自动验证，无需人工逐一检查。数周内，这个项目便吸引大量参与者高效完成了任务。

受此启发，2024年9月，陶哲轩启动了更大规模的“等式理论”项目。这次，他提出一个包含约4694条代数定律、涉及2200万条逻辑蕴含关系的庞大问题。志愿者团队使用基础编程脚本和自动定理证明器协同工作，几天内就完成了99%的验证。尽管项目后期因剩余难题进展放缓，但已成功发现一种全新的数学结构——“岩浆上同调”，这连长期研究上同调的数学家巴埃兹都表示前所未见。

陶哲轩将这一模式比作物理学从“个人理论推演”到“大型对撞机协作”的进化。他认为，AI虽然暂时无法取代人类数学家解决前沿独创问题，但特别适合处理那些能拆分成成千上万个微小任务的复杂问题。在这些领域，AI可以承担大量基础性子问题求解，并由人类负责最后的难点攻克。

如今，作为美国总统科技顾问委员会成员及生成式AI工作组联合主席，陶哲轩正积极推广这一“实验数学”新范式。他表示，“等式理论”项目已证明了这种新方法的可行性——数学不仅能被大规模协作完成，还能通过实验方式发现意想不到的新成果。对于这位早已功成名就的数学天才来说，这不仅仅是一次技术尝试，更是一场他亲手推动的学科范式转变。

中文翻译：

陶哲轩如何成为人工智能在数学领域的布道者

引言

下文改编自凯文·哈特尼特所著的《代码中的证明：一台真理机器如何改变数学与人工智能》。

陶哲轩从不畏惧非传统思想。2014年11月，他作为五位杰出数学家组成的小组成员出席了一场活动，这五位都是首届突破奖数学奖得主，该奖项附带300万美元奖金。几位获奖者的话题广泛，从数学是被发明还是被发现的（大多数数学家认同，至少感觉上是一种发现行为），到评估我们生活在数字模拟中的可能性。"没错，我认为我们实际上并非真实存在，"马克西姆·孔采维奇说道，他在20世纪90年代在数学与物理的交叉领域完成了其最重要的工作。

然而，在40分钟的讨论中，最令人难以置信的发言来自陶哲轩。他预测，未来数学家可能不是独自工作或组成两三人小组，而是同时与数百人合作项目。他还以谦逊低调的方式表示，当这些合作结束时，结果可能不是由人类审稿人核查，而是由计算机来核查。"总有一天，我们可能不再用LaTeX撰写论文，而是用一种语言，某种智能软件会将其转换为形式化语言，然后你经常会收到编译错误——计算机不理解你是如何推导出这一步的，"他说。

这番话让活动主持人及其他获奖者觉得，相比之下，连模拟假说都显得合理了。比数百名数学家一起工作这个想法更令人惊讶的是，这种合作方式竟会对陶哲轩有吸引力——因为如果说世界上有谁似乎很适合单打独斗，那非他莫属。

陶哲轩1975年出生于澳大利亚阿德莱德，三年后他的父母从香港移民到该国。他作为长子的与众不同之处很早就显现出来。陶哲轩两岁时，全家去朋友家做客，父母发现他和几个六岁孩子聚在一起，演示如何用木块数数。当被问及如何学会数东西时，他回答说是在《芝麻街》上看到的。五年后，陶哲轩七岁时，开始学习微积分。

1985年春天，陶哲轩的父母带他来到美国三周，会见了当时在约翰霍普金斯大学的数学早慧少年研究项目主任朱利安·斯坦利。斯坦利称陶哲轩是他见过的最具数学天赋的人。同年，陶哲轩在著名数学家保罗·埃尔德什访问阿德莱德时见到了他。一张著名照片显示，当时72岁、慈父般的埃尔德什正阅读膝上的一份文件，而10岁、留着浓密黑发的陶哲轩则专注地看着，手指若有所思地托着下巴。

1986年，陶哲轩参加国际数学奥林匹克竞赛，年少成名就此延续。第一年他获得铜牌，以10岁的年龄成为该成绩的最年轻选手。随后两年，他成为最年轻的银牌得主，最终也成为最年轻的奥运金牌得主。他的正规教育也以同样加速的节奏进行。15岁时，他从当地的阿德莱德弗林德斯大学毕业，并于1992年秋天与父亲一同登上飞往新泽西的飞机，开始在普林斯顿大学攻读数学博士学位。埃尔德什曾为陶哲轩提前入学项目背书，在推荐信中写道："我相信他会成长为一位一流的数学家，或许会成为一位真正伟大的数学家。"

埃尔德什说对了。到24岁时，陶哲轩已做出足够多的新发现，可以任意选择终身教职岗位；他最终决定在加州大学洛杉矶分校定居。大约在那时，他遇到了一位年轻的英国数论学家本·格林。两人开始合作证明一个命题：某些被称为算术级数的模式（即集合中的数字按固定间隔递增，如7、10、13、16）必然出现在大量素数集合中，尽管素数在数轴上看似随机分布。他们的证明成为陶哲轩早期职业生涯的标志性成果，助力他于2006年获得菲尔兹奖，并将他推向了数学界的最上层。

陶哲轩本可以不与任何人合作就建立起成功的职业生涯，但这不是他喜欢的工作方式。他认为与其他研究者合作是发现新想法的主要途径——用你已知的，结合我已知的，看看会发生什么。

这种方法使陶哲轩的数学研究涵盖了异常广泛的课题，从解析数论（包括关于素数的格林-陶定理），到分析学（研究描述流体行为的纳维-斯托克斯方程的性质），再到从数字数据构建磁共振成像图像的算法。（磁共振成像合作源于陶哲轩与时任加州理工学院统计学家的伊曼纽尔·坎德斯的对话，两人当时都在送孩子上幼儿园。）这种对合作发现的渴望也促使陶哲轩公开进行许多工作。2007年，他开设了一个博客，开始定期发布其研究的动态。到那时，陶哲轩不仅是其领域内，也是世界上最著名的数学家之一。他的博文受到大量关注，有时会在评论区引发长篇讨论，陶哲轩也热情参与其中。他这样做是因为觉得有趣，也因为他希望讨论能激发新想法。

大约在同一时期，另一位早期数学博主也有类似想法。与陶哲轩一样，蒂莫西·高尔斯也是一位杰出的研究型数学家，热衷于公开交流。但高尔斯并不指望在博客评论区碰运气，而是希望以集中的方式引导公众能量。2009年1月，他发表了一篇博文，宣布希望能促成一种新型的"大规模协作数学"。他将在一个开放的在线论坛上提出一个问题，"任何对这个问题有话说的人都可以参与进来"。他将其命名为"多面体项目"。

陶哲轩随即加入。与高尔斯一样，他明白有些数学问题比其他问题更适合通过大规模协作来解决。关键是，正如陶哲轩在高尔斯最初博文下的评论中所写，要找到那些能够"产生许多更简单的子问题……且这些子问题在很大程度上可以并行处理"的问题。通过将大问题分解成单个案例，不同团队或个人可以各自独立工作，然后将结果作为更大整体的拼图组合起来。同时，陶哲轩知道，多面体模式可能面临的最大挑战是组织工作：审核贡献并确保所有贡献都是正确的。

对于第一个多面体项目，高尔斯提议改进一个称为哈勒斯-朱伊特定理的结果，该定理涉及用一种颜色或另一种颜色填充网格单元格时出现的模式。经过几个月的工作，通过数十位数学家的数千条评论协调，该小组证明了关于这些着色模式如何出现的更精确陈述。那年秋天，他们以一篇独一无二的数学论文形式发布了成果，署名使用了化名"D.H.J. Polymath"。高尔斯的实验取得了成功。它使得许多数学家（无论是专业还是业余）能够共同合作，并最终得出了一个证明。

在接下来的十年里，又开展了15个多面体项目，其中一些由陶哲轩领导，该计划也引起了主流关注。2011年10月29日，《华尔街日报》发表了一篇题为《新一代爱因斯坦将是乐于分享的科学家》的文章，报道称多面体项目"开创了解决问题的新方法"。

然而，在其他方面，多面体项目是个理念超前于时代的产物。陶哲轩发现身处数学活动的热潮中心令人兴奋，但他也认识到博客评论区作为协作平台存在局限。大规模开放式协作增加了偶然发现的几率，但同时也加剧了众多参与者中有人犯错的风险。防止错误的唯一方法是由管理员仔细检查所有工作。但这种审核瓶颈削弱了多面体的愿景。

陶哲轩真正追求的是一种高效的新型科学发现模式。过了一段时间，他意识到多面体模式并非如此。他认为，要实现这一点，需要某种计算机验证——一种自动而非手动检查贡献的方法。但鉴于2010年代的科技水平，他这个愿望与期盼开设火星客运服务相差无几。

陶哲轩多年来一直知晓计算机验证数学的存在。他知道一些成功案例，但也明白形式化数学仍然不切实际，在大多数情况下需要付出远超其价值的努力。尽管如此，陶哲轩对其潜力仍很着迷。在世界顶尖数学家中，几乎独他一人看到了做数学的新方法的前景。

2022年7月，部分出于满足好奇心，陶哲轩开始组织一场研讨会，探讨计算机辅助数学研究的所有不同方式。他组建了一个联合组织团队，其中包括凯文·巴扎德，后者当时是世界最著名的形式化数学布道者。

开会前，陶哲轩认为Lean（一种允许将数学证明编写并作为计算机代码进行验证的软件）是一个需要数月时间学习的复杂程序。巴扎德说服他试一试。除了受到鼓励，陶哲轩也深感有责任以身作则——如果他要继续推动机器辅助证明，就必须开始亲身体验。

2023年10月9日，陶哲轩在社交媒体上发帖："我已决定最终熟悉 #Lean4 交互式证明系统（必要时使用AI辅助来帮助我使用它）。"

在数学家的热门在线讨论论坛MathOverflow上，陶哲轩发现了一个关于麦克劳林不等式的问题。他决定将其作为形式化实验来回答。首先，他将证明写成典型的数学论文。篇幅简短，只有10页。然后，他将注意力转向真正目标：看看能否用Lean将这一简单证明形式化。

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

在普通论文中，陶哲轩无需费时即可断言：如果你有三个数，且都大于1，那么它们的和必然至少为3。但Lean不接受断言，陶哲轩不得不花时间在Mathlib（Lean用户在编写证明时使用的已形式化数学的数字库）中查找一个引理，以证明这个不言自明的关系。类似地，在非形式化数学中，并不总是需要指明你在哪个数系中工作。例如，数字3同时是整数、自然数和实数。在他最初的论文中，陶哲轩可以简单地写"3"，而不指明他心目中是哪一种3。然而，在Lean中他必须详细说明。陶哲轩发现他的证明一直无法编译，因为他在形式化的不同阶段忽略了指定正确的类型。直到近一个月后，11月6日，陶哲轩才在其博客评论中发帖："只是说明一下，我已经成功地将这篇论文的结果在Lean4中形式化了。"结果微不足道，他为此编写的Lean代码也很糟糕。然而，陶哲轩现在正式成为Lean社区的一名贡献成员。

在学习Lean的同时，陶哲轩继续从事其他一系列研究项目。其中包括与他的长期合作者本·格林和蒂莫西·高尔斯，以及格林的前学生、现任加州大学圣地亚哥分校教授的弗雷迪·曼纳斯合作的项目。这是一个精英合作团队——高尔斯与陶哲轩一样是菲尔兹奖得主，而格林是该领域获得荣誉最多的数论学家之一。

该小组瞄准了一个特定问题，涉及一个称为"和集"的数学对象。如果你有一个数字集合，可以用它来形成另一个相关集合：它的和集。和集是通过取第一个集合中每一对唯一数字的和来构成的。所有这些和一起构成了原始集合的和集。

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

除了具有较小的和集，数字1到10也是算术级数的一个例子，因为它们以恒定间隔递增。计算机科学家考陶琳·马尔通在20世纪60年代提出的猜想断言这并非巧合。她预测，产生小和集的集合必然也包含长的算术级数。高尔斯、格林和陶哲轩在本世纪初曾在称为多项式弗里曼-鲁扎猜想的一个更精细版本上取得进展，但最终陷入困境。然后，在2023年，陶哲轩、格林和曼纳斯再次拾起这个问题，着眼于引入曼纳斯开发的概率论技术。

他们意识到，将这些技术与高尔斯的早期想法结合起来，或许能完全解决这个问题。他们将高尔斯纳入合作，四人小组在2023年夏季稳步推进。到深秋时节，他们成功了。11月9日——就在陶哲轩将他第一个正式的Lean证明上传到GitHub三天后——他们将证明上传到了arxiv.org。

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

然而，格林、高尔斯和曼纳斯并不特别有兴趣花时间学习Lean。于是陶哲轩独自开始——尽管他知道自己可能不会孤单太久。他领导的任何项目都可能引起关注。

11月13日，陶哲轩在一个以Lean为中心的聊天群中开辟了一个新频道。"大家好。我正在考虑启动一个项目，将蒂莫西·高尔斯、本·格林、弗雷迪·曼纳斯和我本人最近关于多项式弗里曼-鲁扎（PFR）猜想的证明在Lean4中形式化，"他写道。他将用这个频道来协调项目活动，并"乐意欢迎志愿者以他们认为自己能够胜任的任何身份为这个项目做出贡献"。这是多面体项目的重启，只不过这次他们是在形式化一个已有的结果，而不是试图证明一个新结果——并且所有工作都将由Lean验证，这意味着陶哲轩不必亲自检查。

一天之内，斯德哥尔摩大学的博士生亚埃尔·迪利耶就为该项目建立了粗略的蓝图，将证明分为13个部分。在每个部分，陶哲轩确定了需要形式化的引理和定义序列。在一篇典型的数学论文中，引理（有助于构建更大定理论证的较简单结果）大约有20行长，但为了PFR的形式化，陶哲轩将证明分解为5行长的引理。他的目标是使证明尽可能模块化，允许许多人做出小贡献。

第一周，该讨论串中的大部分活动是关于形式化证明所需的概率论基本概念，这些概念尚不在Mathlib中。具体来说，他们必须形式化香农熵——对数据源（如数字集合）中不确定性或混乱程度的度量。但在形式化数学的同时，陶哲轩和其他人也在第一周里摸索如何共同工作。起初，对话是自由形式的，陶哲轩发帖说明他认为需要做什么，其他人则插话提出如何做的想法，这与多面体项目在博客评论中展开的方式颇为相似。

11月22日，陶哲轩发布了一份包含22个待处理引理的清单，并写道："如果你想认领其中一条或多条引理，请在本讨论串中回复。"回复纷至沓来："我来认领均匀随机变量的熵：)"，伦敦几何与数论学院的博士生保罗·勒佐写道。"我来试试一般的纤维恒等式"，加州大学洛杉矶分校的博士生亚伦·安德森回复道。

口口相传之下，越来越多的数学家加入了这项工作。到11月底，陶哲轩像一位忙乱的志愿者协调员，自己很少编写Lean代码，而是专注于为他人找任务。11月28日，他写道："考虑到随着PFR项目接近完成，我们可能暂时志愿者过剩，我想到了一个可能有人愿意做的额外小任务。"46分钟后，金·莫里森回复说他们已经完成了任务。"哇，真快！谢谢！"陶哲轩回答。

甚至在形式化完成之前，Lean社区就已经开始讨论其意义。特别是，他们争论该项目的高效率是预示着一个快速形式化的新时代，还是反映了陶哲轩个人的非凡影响力。在群讨论串的总结帖中，陶哲轩反思说自己并未编写太多代码。"这实际上让我相当鼓舞，因为它向我表明，数学家有可能领导Lean形式化项目，而无需具备广泛的Lean编程技能（尽管可能至少需要足够的专业知识来陈述引理，即使不证明它们）。"八分钟后，乌得勒支大学的数学家、Mathlib计划负责人约翰·科梅林回复道："我不想立即劫持这个讨论串，"接着质疑陶哲轩在该项目中学到的经验是否具有广泛适用性。"当然，你在这个项目上得到了很多帮助，因为它备受瞩目，"他写道。

科梅林还指出，尽管参与像PFR这样的项目有趣且激动人心，但年轻数学家在申请学术职位时，这类贡献并不会得到认可。"目前，尚不清楚形式化工作者（暂时找不到更好的职位描述）将如何得到数学界的认可，也不清楚这些活动在就业市场上将如何被评估。"陶哲轩回复道："值得一提的是，我非常乐意在推荐信中适当提及对本项目的贡献。"

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

他形成这种观点，部分是因为他看到了当前AI工具的明确局限性。它们在解决简单问题或拥有大量先验数据的任务上表现出色，但在数学的前沿领域——那里发表结果稀少，可用于训练的数据也很少——AI则表现不佳。在他早期对LLM的实验中，他观察到它们表现得像过度自信的本科生，提出建议时缺乏区分好主意与坏主意的专业知识。

然而，陶哲轩心中已有前进方向。他不认为AI会很快取代人类数学家，但他确实认为AI特别适合帮助解决某些类型的复杂数学问题：那些可以分解成数千个易于管理的子问题的问题——本质上与适合多面体项目的同类问题。在这种规模下，数学家可以利用AI解决大量最简单的子问题，将其结果以Lean可以检查的形式化证明输出，然后亲自介入处理最困难的剩余问题。2024年，陶哲轩向所有愿意聆听的人推广这一愿景，并且在PFR项目之后，他意识到如果他真的相信这项工作，他需要挺身而出，亲自领导。他也立刻知道自己将从哪个问题入手。

这是他一年前偶然遇到的一个问题。2023年7月，MathOverflow上的一位用户提出了一个看似简单的谜题。考虑一个像加法这样的运算，该用户写道。它可能遵循某些基本代数定律，如交换律（x + y = y + x）或结合律（(x + y) + z = x + (y + z)）。在许多情况下，定律之间没有关系——例如，交换律并不蕴含结合律。

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

但定律之间普遍如何关联的问题引起了陶哲轩的好奇。他不满足于逐一解决谜题，而是开始勾勒一个粗略的图表，展示不同可能代数定律之间的关系。很明显，这个图景可能相当复杂。

他发现，如果将自己的研究限制在涉及恰好四次运算的代数定律上，大约有4694条定律需要他来处理。每条定律可能蕴含或不蕴含任何其他定律，产生了2200万个逻辑蕴含关系需要检查。一旦他全部检查完毕——要么通过证明它们成立，要么通过找到它们不成立的反例——他将拥有这4694条定律如何相互关联的完整图景。这感觉正好适合他提出的数学新风格。

陶哲轩将他的新努力命名为"等式理论"，并于2024年9月25日在其个人博客上发帖宣布成立。他开篇列举了过去大规模公开数学合作困难的主要原因，然后写道："证明助手语言，如Lean，提供了克服这些障碍的潜在方法。"

首先，陶哲轩和越来越多的志愿者用被称为"岩浆"的简单数学结构测试了超过4000条定律。岩浆是算术的简化版本，是一个有用的起点，因为任何对岩浆不成立的定律都不可能蕴含其他更复杂的定律。参与者使用基本的Python脚本迅速测试了数百万个这样的简化系统，并在几天内解决了2200万个潜在蕴含关系中超过99%的问题。陶哲轩在第二天（9月27日）发帖称，他对项目的进展速度感到惊讶："这个项目的进展远远、远远快于我预期，扩展速度也大大超过预期——仅48小时，很大一部分蕴含关系很可能很快就能解决！我以为三周的PFR项目很快，但这个速度简直是疯狂的另一个层次。"

一旦最简单的蕴含关系得到解决，等式理论项目的志愿者便以去中心化的方式转向自动化定理证明器，这些证明器可以自行搜索问题的解决方案，无需交互式帮助。这些证明器，加上老式的人类智慧，逐个攻克了未解决的问题。

如同科学家看着自己的造物活过来一般，陶哲轩欣赏着正在展开的工作。"项目似乎成功地实现了去中心化；特别是，现在正在进行许多我都不完全了解的活动，"他写道。

对许多数学家来说，陶哲轩的项目既有趣又古怪。巴扎德关注着它，被这个社会实验所吸引，尽管对等式理论的数学内容感到无聊。他认为这既基础又古怪，尽管他钦佩陶哲轩的创造力。另一位著名数学家约翰·贝兹则更为直言不讳。他评论道："对我来说，这似乎是在大规模浪费时间，"随后承认他对大学橄榄球也有同感，而很多人同样喜欢它。

一个月内，等式理论小组将2200万个问题缩减到238个。到11月下旬，他们减少到138个。随着他们逐渐攻克剩余案例，进展放缓。新年伊始，大约有30个蕴含关系仍未解决，进展速度进一步放缓。到3月底，他们已卡在最后四个上数周之久。贡献者们尝试处理剩余部分，但剩下这么少的蕴含关系，许多人便离开了；陶哲轩的更新频率从近乎每日一次降至每几周一次。

然而，解决2200万个蕴含关系中的每一个从来都不是等式理论的真正目标。纯粹出于好奇，陶哲轩想要一张完整图景的地图，而现在他有了，只差几个细节。更重要的是，他将等式理论视为一种从根本上做数学的新方式的试点项目——在这方面，它取得了无可挑剔的成功。

在陶哲轩看来，等式理论是他所希望成为"实验"数学新纪元的前奏。他设想的是物理学等领域已经经历的那种变革。物理学曾经在很大程度上是一门理论学科，孤独的思想者或小型合作团队一次解决一两个问题——换句话说，它曾经看起来很像现在的数学。但随着技术的进步，该领域涌现出一个新的实验分支——像欧洲核子研究中心的大型强子对撞机那样的实验室里的大规模合作，数百甚至数千名拥有专业技能的研究人员共同努力，产生了海量数据。这些实验并没有取代理论，而是相辅相成，新结果在两种研究模式之间流动。

陶哲轩设想数学也会发生类似的演变。他相信，新颖的探究形式将不可避免地带来新颖的洞见，正如以往那样。当等式理论团队系统地从他们庞大的表格中划掉蕴含关系时，他们偶然发现了一些真正新颖的数学构造——比如"岩浆上同调"，这是群上同调概念的一个奇特扩展，群上同调是一个深入且被充分研究的领域，描述群何时可以或不能以特定方式扩展。陶哲轩联系了约翰·贝兹（对等式理论持否定态度者，也是上同调专家），询问这个构造以前是否出现过。贝兹承认他从未见过。

对陶哲轩来说，这正是关键所在。该项目表明，数学可以用不同的、实验性的方式进行——并且在此过程中，确实生成了真正新的东西。陶哲轩从未期望等式理论会挖掘出一个重大发现；他希望它展示一种新型数学机器的有效性。从这个意义上说，它成功了。陶哲轩找到了一种做数学的新方法，并且没有任何重返旧途的迹象。

摘自凯文·哈特尼特所著《代码中的证明：一台真理机器如何改变数学与人工智能》。版权 © 2026 归凯文·哈特尼特所有。将于2026年6月9日由Quanta Books与Farrar, Straus and Giroux合作出版。保留所有权利。

英文来源：

How Terry Tao Became an Evangelist for AI in Math
Introduction
The following has been adapted from The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett.
Terry Tao has never been afraid of unconventional ideas. In November 2014, he was on a panel of five distinguished mathematicians, all inaugural recipients of the Breakthrough Prize in Mathematics, which came with a $3 million award. The laureates’ conversation ranged from whether mathematics is invented or discovered — most of the mathematicians agreed that, at the very least, it feels like an act of discovery — to an assessment of the odds that we’re living in a digital simulation. “Yeah, I think we’re actually not real,” said Maxim Kontsevich, who did his most important work in the 1990s at the intersection of math and physics.
Yet over the course of the 40-minute discussion, the statements that drew the most incredulity were Tao’s. He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers. “One day we may actually write our papers not in LaTeX, but in some language which some smart software will convert to a formal language, and every so often you’ll get a compilation error — the computer does not understand how you derived this step,” he said.
The statement was greeted by the event moderator and the other laureates as preposterous enough to make the simulation hypothesis seem reasonable by comparison. Even more surprising than the idea of hundreds of mathematicians working together was the fact that such a collaboration would appeal to Tao — because if anyone in the world seemed well suited to going it alone, it was him.
Tao was born in 1975 in Adelaide, Australia, three years after his parents immigrated to the country from Hong Kong. The first signs that their firstborn son was different came early. When Tao was 2 and his family was visiting friends, his parents found him gathered with several 6-year-olds, demonstrating how to count using wooden blocks. Asked how he’d learned to count things, he responded that he had seen it on Sesame Street. Five years later, when Tao was 7, he began learning calculus.
For three weeks in the spring of 1985, Tao’s parents brought him to the United States, where he met with Julian Stanley, director of the Study of Mathematically Precocious Youth, then at Johns Hopkins University. Stanley described Tao as having the greatest mathematical ability he had ever seen. That same year Tao met the acclaimed mathematician Paul Erdős during the latter’s visit to Adelaide. A famous picture shows the grandfatherly Erdős, 72 at the time, reading a document in his lap while Tao, 10 years old with thick black hair, looks on intently, fingers raised thoughtfully to his chin.
Tao’s young legend grew when he entered the International Math Olympiad in 1986. He won a bronze medal that first year, becoming, at the age of 10, the youngest competitor ever to achieve that result. In the two succeeding years he became the youngest-ever silver medalist and finally the youngest person ever to win a gold medal. His formal education proceeded at a similarly accelerated pace. He graduated from the local Flinders University in Adelaide when he was 15 and, in the fall of 1992, boarded a plane with his father for New Jersey, where he started a Ph.D. in math at Princeton University. Erdős had endorsed Tao’s early admission to the program, writing in a letter of recommendation, “I am sure he will develop into a first-rate mathematician and perhaps into a really great one.”
Erdős was right. By the time Tao was 24, he had made enough new discoveries to have his choice of permanent faculty positions; he ultimately decided to settle at the University of California, Los Angeles. Around that time, he met a young English number theorist named Ben Green. The two began collaborating on a proof that certain kinds of patterns called arithmetic progressions — in which the numbers in a set increase by a fixed interval, like 7, 10, 13, 16 — inevitably appear in large collections of prime numbers, despite the fact that primes appear to be scattered randomly along the number line. Their proof would become the signature result of Tao’s early career, contributing to his winning the Fields Medal in 2006, and propelling him to the upper echelons of mathematics.
Tao could have built a successful career without collaborating with anyone, but that’s not the way he liked to work. He viewed working with other researchers as a primary way to discover new ideas — take what you know, pair it with what I know, and see what happens.
This approach led Tao’s mathematical research to range over an unusually broad set of topics, from analytic number theory, including the Green-Tao theorem about prime numbers, to analysis, where he studied properties of the Navier-Stokes equations that describe the behavior of fluids, to algorithms for constructing MRI images from digital data. (The MRI collaboration developed during conversations Tao had with Emmanuel Candès, a statistician then at the California Institute of Technology, while they were both dropping off their kids at preschool.) This thirst for collaborative discovery also led Tao to do a lot of his work in public. In 2007, he started a blog, where he began publishing regular updates about his research. By that point, Tao was one of the most famous mathematicians not only in his field but in the world. His posts received a lot of attention and sometimes led to long exchanges in the comments section, where Tao enthusiastically participated. He did it because he found it fun, and because he hoped the conversation might generate new ideas.
Around that time, another early math blogger had a similar thought. Like Tao, Timothy Gowers was a prominent research mathematician with a taste for public exchange. But rather than trusting serendipity to strike in his blog’s comment section, Gowers wanted to channel public energy in a focused way. In January 2009, he published a blog post announcing his desire to facilitate a new kind of “massively collaborative mathematics.” He would propose a problem in an open online forum, and “anybody who had anything whatsoever to say about the problem could chip in.” He named it the Polymath Project.
Tao jumped in. Like Gowers, he understood that some math problems were more amenable than others to being solved through large-scale collaboration. The key, as Tao wrote in a comment on Gowers’ initial post, was to find problems that could “generate a number of simpler sub-problems … which can largely be worked on in parallel.” By breaking big problems into individual cases, different teams or individuals could work on their own and then assemble their results as pieces of a bigger whole. At the same time, Tao knew that perhaps the biggest challenge with the Polymath model would be organizing: moderating contributions and checking to make sure that all the contributions were correct.
For the first Polymath project, Gowers proposed improving a result called the Hales-Jewett theorem, which was about patterns that appear when you shade cells in a grid with one of two different colors. After a few months of work, coordinated through thousands of comments by dozens of mathematicians, the group had proved a more exact statement about how those coloring patterns emerge. That fall, they released the work as a first-of-its-kind math paper with the pseudonymous byline “D.H.J. Polymath.” Gowers’ experiment had been a success. It allowed many mathematicians — professional and amateur alike — to work together and yielded a proof in the end.
Over the next decade, there were 15 more Polymath projects, some of which Tao led, and the initiative attracted mainstream attention. On October 29, 2011, The Wall Street Journal ran an article called “The New Einsteins Will Be Scientists Who Share” and reported that the Polymath Project had “pioneered a new approach to problem-solving.”
Yet in other ways, the Polymath Project was an idea before its time. Tao found it exhilarating to be at the center of a frenzy of mathematical activity, but he recognized that the comments section of a blog was a limited platform for collaboration. Massive open collaboration increased the likelihood of a certain kind of serendipitous discovery, but at the same time it heightened the odds that any one of the many participants would contribute a mistake. The only way to guard against error was for a moderator to carefully check all the work. But that kind of moderation bottleneck undermined the Polymath vision.
What Tao was really after was an efficient new form of scientific discovery. And after a while, he came to understand that the Polymath model was not it. To make it real, he thought, some kind of computer verification would be needed — a way to check contributions automatically, rather than by hand. But given the state of technology in the 2010s, he might as well have wished for passenger service to Mars.
Tao had been aware of computer-verified mathematics for years. He knew about a few success stories, but he also knew that formal math was still impractical, requiring far more effort than it was worth in most cases. Nevertheless, Tao was intrigued by its potential. Almost uniquely among the world’s elite mathematicians, he saw the potential in new methods for doing mathematics.
In July 2022, in part to satisfy his curiosity, he began to organize a workshop on all the different ways computers were assisting mathematical research. He brought on a team of co-organizers, including Kevin Buzzard, who was at the time the world’s most visible evangelist for formal mathematics.
Going into the conference, Tao regarded Lean, software that allows mathematical proofs to be written and checked as computer code, as a complicated program that would take months to learn. Buzzard convinced him to give it a try. Along with that encouragement, Tao felt a strong responsibility to lead by example — if he was going to continue promoting machine-assisted proof, he needed to start trying it himself.
On October 9, 2023, Tao posted on social media, “I have decided to finally get acquainted with the #Lean4 interactive proof system (using AI assistance as necessary to help me use it).”
On MathOverflow, a popular online discussion forum for mathematicians, Tao found a question about something called Maclaurin’s inequality. He decided to answer it as an experiment in formalization. First, he wrote up the proof as a typical math paper. It was short, only 10 pages long. Then he turned his attention to his real goal: seeing if he could formalize the simple proof in Lean.
Initially, Tao thought he might be able to do it in a week, but he was quickly confronted by the differences between writing math by hand and typing it in Lean. Tao observed that the hard parts of the proof were easy to formalize in Lean, while the simple parts took a surprising amount of work.
In the regular paper, Tao spent no time at all asserting that if you have three numbers, all of which are greater than 1, their sum is necessarily at least 3. But Lean doesn’t abide assertions, and Tao had to spend time digging up a lemma in Mathlib — a digital library of already-formalized mathematics that Lean users draw on when writing proofs — that proved the self-evident relationship. Similarly, in informal math, it’s not necessary to always specify which number system you’re working in. The number 3, for example, is simultaneously an integer, a natural number, and a real number. In his original paper, Tao could simply write “3” without specifying what kind of 3 he had in mind. However, in Lean he had to spell it out. Tao found his proof kept failing to compile because he had neglected to specify the correct type at different points in the formalization. It wasn’t until nearly a month later, on November 6, that Tao posted in a comment on his blog, “Just a remark that I have managed to formalize the results of this paper in Lean4.” The result was minor, and the Lean code he had written to formalize it was terrible. Yet Tao was now officially a contributing member of the Lean community.
At the same time he was learning Lean, Tao continued work on a host of other research projects. These included one with his longtime collaborators Ben Green and Tim Gowers, as well as Freddie Manners, a former student of Green’s and now a professor at the University of California, San Diego. It was an elite set of collaborators — Gowers, like Tao, had won a Fields Medal, while Green was among the most decorated number theorists in the field.
The group had a particular problem in their sights, one that revolved around a mathematical object called a sumset. If you have a collection of numbers, it can be used to form another, related collection: its sumset. The sumset is made by taking the sum of every unique pair of numbers in the first set. All those sums together form the sumset of the original set.
If the original set is full of random numbers, then its sumset will be comparatively large. A set of 10 random numbers has a sumset of about 50 numbers (and a set of 1,000 numbers has a sumset of about 500,000 numbers). But if, instead of containing random numbers, the original set follows some kind of pattern, its sumset will be much smaller because many sums will appear multiple times (and you only include each sum once in the sumset). The set of the numbers 1 to 10 is one example — its sumset only contains 17 numbers (not 50, as you’d expect if it were a random collection of 10 numbers), because many of the sums repeat (1 + 6, 2 + 5, and 3 + 4 all equal 7, and you only enter 7 once in the sumset).
In addition to having a small sumset, the numbers 1 through 10 are an example of an arithmetic progression because they increase by a constant interval. A conjecture with roots in the 1960s by the computer scientist Katalin Marton asserts that this isn’t a coincidence. She predicted that sets that produce small sumsets must also include long arithmetic progressions. Gowers, Green, and Tao had made headway on a refined version of this problem called the polynomial Freiman-Ruzsa conjecture in the early 2000s but eventually got stuck. Then, in 2023, Tao, Green, and Manners picked it up again with an eye toward introducing techniques from probability theory that Manners had developed.
They realized that by combining those techniques with Gowers’ earlier ideas, they might be able to solve the whole thing. They brought Gowers into the collaboration, and the quartet made steady progress through the summer of 2023. By late fall, they had it. On November 9 — just three days after Tao uploaded his first formal Lean proof to GitHub — they uploaded their proof to arxiv.org.
With Lean on his mind, Tao suggested to his three co-authors that they could try formalizing their paper. The work seemed like a good candidate for formalization both because it was an important result and because it relied on relatively simple techniques. They wouldn’t have to spend months adding prerequisite material to Mathlib — most of the necessary definitions were already there.
However, Green, Gowers, and Manners weren’t especially interested in taking the time to learn Lean. So Tao set off on his own — though he knew he likely wouldn’t be alone for long. Any project he led was likely to draw attention.
On November 13, Tao kicked off a new channel in a Lean-focused chat group. “Hi everyone. I am thinking of starting a project to formalize in Lean4 the recent proof of Timothy Gowers, Ben Green, Freddie Manners, and myself of the polynomial Freiman-Ruzsa (PFR) conjecture,” he wrote. He would use the channel to coordinate activity on the project and would be “happy to accept volunteers to contribute to this project in whatever capacity they feel able.” It was a reboot of the Polymath Project, only this time they were formalizing an existing result rather than trying to prove a new one — and all the work would be verified by Lean, meaning Tao wouldn’t have to check it himself.
Within a day, Yaël Dillies, a Ph.D. student at Stockholm University, had set up a rough blueprint for the project that divided the proof into 13 sections. Within each section, Tao identified the sequence of lemmas and definitions that needed to be formalized. In a typical math paper, lemmas — simpler results that help build toward the proof of a larger theorem — might be about 20 lines long, but for the PFR formalization, Tao broke the proof down into five-line lemmas. His goal was to make the proof as modular as possible, allowing many people to make small contributions.
For the first week, most of the activity on the thread was about formalizing basic concepts from probability theory that the proof required but were not yet in Mathlib. In particular, they had to formalize Shannon entropy — a measure of the uncertainty or disorder in a data source, like a set of numbers. But along with formalizing math, Tao and the others spent that first week figuring out how to work together. Initially, the conversation was free-form, with Tao posting about what he thought needed to be done and others chiming in with ideas about how to do it, much as the Polymath projects had unfolded in blog comments.
On November 22, Tao posted a list of 22 outstanding lemmas and wrote, “If you want to claim one or more of these lemmas, please do so by replying in this thread.” The replies flooded in: “I’d like to claim the entropy of a uniform random variable :),” wrote Paul Lezeau, a Ph.D. student at the London School of Geometry and Number Theory. “I’m gonna take a stab at the general fibring identity,” replied Aaron Anderson, a Ph.D. student at UCLA.
Drawn by word of mouth, more and more mathematicians joined the effort. By the end of November, Tao, like a harried volunteer coordinator, was writing little Lean code himself, instead focusing on finding tasks for others to do. On November 28, he wrote, “Given that we may temporarily have a surplus of volunteers for the PFR project as it nears completion, I thought of one additional small task that someone might be willing to work on.” Forty-six minutes later, Kim Morrison replied that they had completed the task. “Wow, that was quick! Thanks!” Tao answered.
Even before the formalization was complete, the Lean community began discussing what it meant. In particular, they debated whether the efficiency of the project signaled a new era of fast formalization, or whether it reflected the singular influence of Terry Tao. In a wrap-up post in the group thread, Tao reflected that he had not written much of the code himself. “This is actually quite encouraging to me, as it suggests to me that it will be possible for mathematicians to lead Lean formalization projects without requiring extensive Lean programming skills (though one may need at least enough expertise to be able to state lemmas, if not prove them).” Eight minutes later, Johan Commelin, a mathematician at Utrecht University and the director of the Mathlib initiative, replied, “I don’t want to immediately hijack this thread,” before going on to question whether the lessons Tao had learned during the project were broadly applicable. “Of course you got a lot of help with this project because of its high-profile nature,” he wrote.
Commelin also noted that while projects like PFR were fun and exciting to take part in, contributing to them was not the kind of thing young mathematicians were recognized for when they applied for academic jobs. “At the moment, it is still not clear how formalizers (for lack of a better job description) will be credited by the mathematical community, and how these activities will be valued on the job market.” Tao replied, “For what it’s worth, I’m more than happy to mention contributions to this project in letters of reference as appropriate.”
By 2024, Tao had become the most prominent public voice touting the potential of machine-assisted mathematics. He was three years into his tenure on President Joe Biden’s President’s Council of Advisors on Science and Technology and had become co-chair of a working group on generative AI. In a pair of high-profile speeches in 2024, he expressed his vision for a new kind of mathematical collaboration: one that combined human insight, the creativity of large language models, and the guarantees of correctness provided by formal verification systems.
He came to this view in part because he saw clear limits on what current AI tools could do. They excelled at solving straightforward problems or tasks with plenty of prior data, but at the frontier of mathematics — where there were few published results and little data to train on — AI faltered. In his early experiments with LLMs, he observed that they behaved like overconfident undergraduates, offering suggestions without the expertise to tell the difference between good and bad ideas.
Yet Tao had a way forward in mind. He didn’t think AI would replace human mathematicians anytime soon, but he did consider it particularly well suited to helping solve certain types of complex mathematical problems: ones that could be broken into thousands of small, manageable subproblems — essentially the same class of problems that worked well for Polymath projects. At that scale, mathematicians could employ AI to solve large swaths of the easiest subproblems, with its results outputted as formal proofs that Lean could check, and step in to handle the most difficult remaining questions themselves. In 2024, Tao was promoting this vision to anyone who would listen, and following the PFR project, he had realized that if he really believed in the work, he needed to step up and lead it himself. He also knew right away which problem he would start with.
It was a question that he had stumbled upon a year earlier. In July 2023, a user on MathOverflow posed a seemingly simple puzzle. Consider an operation like addition, the user wrote. It might follow certain fundamental algebraic laws like the commutative law, which says x + y = y + x, or the associative law, which states that (x + y) + z = x + (y + z). In many cases, there’s no relationship between one law and another — the commutative law doesn’t imply the associative law, for example.
The MathOverflow question concerned the relationship between two particular laws, and another user answered it quickly.
But the question of how laws relate to each other in general caught Tao’s curiosity. Rather than solving puzzles one by one, Tao began sketching out a rough diagram that showed how different possible algebraic laws relate to one another. It became clear the picture might be quite complicated.
He saw that if he restricted his study to algebraic laws involving operations applied exactly four times, there were about 4,694 laws he had to account for. Each law could potentially imply or fail to imply any other law, creating 22 million logical implications to check. Once he had checked them all — either by proving they held or by finding a counterexample in which they failed — he would have a complete picture of how all 4,694 of those laws relate to each other. It felt like exactly the right scale for the new style of mathematics he was proposing.
Tao called his new endeavor “Equational Theories” and announced its formation in a post on his personal blog on September 25, 2024. He opened by ticking through the main reasons large-scale public math collaborations had been hard in the past and then wrote, “Proof assistant languages, such as Lean, provide a potential way to overcome these obstacles.”
To start, Tao and the growing number of volunteers who joined him tested the more than 4,000 laws against simple mathematical structures known as magmas. Magmas are stripped-down versions of arithmetic that made for a useful starting point because any law that failed to hold for magmas couldn’t possibly imply other, more complex laws. The participants quickly tested millions of these simplified systems using basic Python scripts and within days had resolved more than 99% of the 22 million potential implications. Tao posted on day 2 — September 27 — that he was astonished at how rapidly the project was advancing: “This project has moved far, far quicker, and scaled up much much faster, than I had expected — only 48 hours in and already a large fraction of the implications are likely to be resolved soon! I thought the 3-week PFR project was fast, but this is an insane additional level of speed.”
Once the simplest implications were resolved, the Equational Theories volunteers moved in a decentralized way to automated theorem provers that could search for solutions to problems all on their own, without interactive help. These provers, along with old-fashioned human ingenuity, knocked down the open questions one at a time.
Like a scientist watching his own creation come to life, Tao admired the work as it unfolded. “The project seems to be successfully decentralizing; in particular, there is now a lot of activity going on now that I am not fully aware of,” he wrote.
To many mathematicians, Tao’s project was intriguing but odd. Buzzard followed along, fascinated by the social experiment though bored by the mathematical content of Equational Theories. He thought it was both elementary and weird, though he admired Tao’s inventiveness. John Baez, another prominent mathematician, was more blunt. He remarked, “This seems like a colossal waste of time to me,” before acknowledging that he felt the same way about college football, and plenty of people liked that, too.
Within a month, the Equational Theories group had narrowed 22 million questions down to 238. By late November, they were down to 138. As they chipped away at the remaining cases, progress slowed. When the new year began, about 30 implications were left unresolved, and the rate of progress slowed even further. By the end of March, they had been stuck for several weeks on just four. Contributors tried their hand at the remainder, but with so few implications left, many people drifted away; Tao’s updates slackened from their near-daily cadence to once every few weeks.
But settling every single one of the 22 million implications had never really been the goal of Equational Theories. Out of sheer curiosity Tao had wanted a map of the complete landscape, and now he had that, minus a few details. More importantly, he viewed Equational Theories as a pilot project for a fundamentally new way of doing mathematics — and in that regard it was an unqualified success.
Equational Theories, in Tao’s view, was the opening act of what he hoped would become a new era of “experimental” mathematics. He had in mind the kind of transformation that had already come to fields like physics. Physics had once been a largely theoretical discipline where solitary thinkers or small groups of collaborators tackled one or two problems at a time — in other words, it used to look a lot like math still did. But with technological advancements came a new, experimental branch of the field — massive collaborations at laboratories like CERN’s Large Hadron Collider, where hundreds or even thousands of researchers with specialized skills worked together and generated huge volumes of data. These experiments didn’t replace theory but complemented it, with new results washing between the two modes of investigation.
Tao imagined a similar evolution happening in mathematics. He trusted that novel forms of inquiry would inevitably lead to novel insights, as they always had before. As the Equational Theories team methodically crossed implications off their immense table, they stumbled onto genuinely new mathematical constructions — like “magma cohomology,” an alien extension of the concept of group cohomology, a deep and well-studied field describing when groups can or cannot be enlarged in certain ways. Tao reached out to John Baez — the Equational Theories naysayer and an expert in cohomology — to ask if this construction had been seen before. Baez admitted he had never encountered it.
To Tao, that was exactly the point. The project had shown that mathematics could be conducted differently, experimentally — and in doing so, it had turned up something genuinely new. Tao had never expected Equational Theories to unearth a revelation; he wanted it to demonstrate the efficacy of a new kind of mathematical machine. And in that sense it worked. Terry Tao had found a new way of doing mathematics, and he showed no signs of going back.
Excerpted from The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett. Copyright © 2026 by Kevin Hartnett. To be published on June 9, 2026, by Quanta Books in partnership with Farrar, Straus and Giroux. All rights reserved.