陶哲轩：引领AI与数学融合的开拓者

人工智能前沿资讯，第一时间为您送达

通过自动化验证工具，复杂的数学问题能够被分解成若干小块（chunks）分别解决，确保每个推理步骤都准确无误，再整合得出最终结果。一些学者认为，这标志着数学研究方式即将迎来重大变革。

像Lean这样的自动化验证工具，可以为数学证明的严谨性提供完全的保障。

图源：Samuel Velasco |《量子杂志》Quanta Magazine

代码致谢：亚历克斯・康托罗维奇（Alex Kontorovich）

作者：Kevin Hartnett（凯文・哈特内特，量子杂志特约撰稿人）2026-6-8

译者：zzllrr小乐（数学科普公众号）2026-6-9

求点赞

求分享

求喜欢

凯文・哈特内特（ Kevin Hartnett ）

本文摘自凯文・哈特内特（Kevin Hartnett）2026年6月出版的新书《代码中的证明：一台真理机器如何重塑数学与AI人工智能》The Proof in the Code: How a Truth Machine Is Transforming Math and AI。

陶哲轩向来乐于接纳非主流的全新理念。2014年11月，他与另外四位杰出数学家共同出席座谈，五人均为首届数学突破奖得主，该奖项奖金高达 300 万美元。座谈期间，众人探讨了诸多话题：数学究竟是人类的创造，还是原本就存在的客观发现？多数数学家认为，至少在研究过程中，数学更像是一种 “发现”；众人还聊到人类或许活在数字虚拟世界中的可能性。马克西姆・孔采维奇（Maxim Kontsevich）是1990年代深耕数学与物理交叉领域的顶尖学者，他直言：“我认为我们当下所处的世界并非真实。”

但在这场长达 40 分钟的交流中，最让众人难以置信的言论，均出自陶哲轩之口。他预言，未来数学家将不再独自钻研，或是仅与两三位同行组成小团队开展研究，而是会和数百名研究者协作攻克课题。他还以一贯谦逊平和的语气补充道：这类大型协作项目完成后，研究成果也不再由人类审稿人核验，而是交由计算机完成。“终有一天，我们撰写学术论文将不再使用 LaTeX 排版语言，而是借助专用软件将文稿转化为形式化语言。编写过程中还会频繁出现编译报错 —— 这意味着计算机无法理解某一步推导逻辑。”

这番话引发了广泛讨论，相比之下，"人类活在虚拟世界" 的猜想反倒显得合情合理。陶哲轩提出大规模协作模式，本身就格外出人意料，因为世人眼中，他本就是最擅长独自深耕研究的数学家。

陶哲轩 1975 年出生于澳大利亚阿德莱德（Adelaide），他的父母三年前从中国香港移民至此。陶哲轩的过人天赋在幼年时期便展露无遗。两岁时，父母带他拜访友人，发现他正和几名六岁的孩子围坐在一起，用积木教大家数数。当被问及从何处学会数数时，他回答是从《芝麻街》Sesame Street节目里学到的。七岁那年，他开始系统学习微积分。

《代码中的证明》一书，探寻人机协作开展数学研究的新时代。

图源：Samuel Velasco / Quanta Magazine

1985年春天，陶哲轩的父母带着他远赴美国，拜访了约翰斯・霍普金斯大学 “数学天赋青少年研究项目” 负责人朱利安・斯坦利（Julian Stanley）。斯坦利评价，陶哲轩是他毕生见过数学天赋最高的孩子。同年，著名数学家保罗・埃尔德什（Paul Erdős）到访阿德莱德，二人得以相遇。一张经典照片记录下当时的场景：彼时 72 岁、须发花白的埃尔德什低头看着手中文稿，年仅十岁的陶哲轩站在一旁，黑发浓密，手托下巴，全神贯注地凝视文稿，陷入沉思。

彼时72岁的保罗・埃尔德什，与年仅十岁的陶哲轩同框。

图源：Billy Grace Tao

陶哲轩的传奇少年之路仍在延续。1986年，他首次参加IMO国际数学奥林匹克竞赛，斩获铜牌，成为该赛事史上最年轻的铜牌得主。此后两年，他接连刷新纪录，先后成为史上最年轻的银牌、金牌获得者。他的求学之路同样一路高歌猛进：15岁便从阿德莱德的弗林德斯大学毕业；1992年秋季，他随父亲前往美国新泽西州，进入普林斯顿大学攻读数学博士学位。埃尔德什曾专门为他撰写推荐信，助力其破格入学，信中写道：“我坚信，他必将成长为一流数学家，甚至有望跻身伟大数学家之列。”

埃尔德什的预判最终成真。24 岁时，陶哲轩已凭借多项重磅研究成果，手握多所顶尖高校的终身教职邀约，最终他选择执教于加州大学洛杉矶分校。也正是在这一时期，他结识了英国顶尖数论学家本・格林（Ben Green）。二人携手开展一项重要证明：即便素数在数轴上看似随机分布，海量素数集合中也必然存在特定规律的等差数列（例如 7、10、13、16，相邻数字差值恒定）。这项成果成为陶哲轩早年职业生涯的代表作，助力他在2006年斩获菲尔兹奖，也让他稳居全球顶尖数学家行列。

即便孤身一人也能成就一番事业，陶哲轩却始终偏爱协作研究。在他看来，与同行交流合作是迸发新思想的核心途径 —— 将彼此的知识融会贯通，便能催生全新发现。

这种研究思路，让陶哲轩的研究版图变得极为广阔：从解析数论（代表作即与格林-陶定理），到分析学（研究描述流体运动的纳维-斯托克斯方程），再到基于数字数据重构核磁共振影像的算法。其中，核磁共振相关研究的缘起十分有趣：当时他与加州理工学院的统计学家埃马纽埃尔・坎德什（Emmanuel Candès）在幼儿园接送孩子，二人闲聊间萌生了合作想法。乐于协作、乐于公开分享研究的特质，促使陶哲轩在 2007 年开设了个人博客https://terrytao.wordpress.com，定期更新研究进展。彼时的他，早已是全球家喻户晓的顶尖数学家。博客文章吸引了大量读者，评论区常常掀起热烈的学术讨论，陶哲轩也会积极参与互动。他坦言，一方面是享受交流的乐趣，另一方面也希望在思想碰撞中收获新灵感。

同期，另一位知名数学家蒂莫西・高尔斯（Timothy Gowers，也是菲尔兹奖得主，译者注）也热衷线上学术交流。但他并不满足于博客评论区零散的灵感碰撞，而是希望组织有目标的大规模公开协作。2009年1月，高尔斯在博客发文，提出打造一种全新的 "大规模协作数学研究模式"：在公开线上论坛抛出数学难题，欢迎所有感兴趣的人建言献策。这一项目被命名为博学者计划（Polymath Project，Polymath既有博学者之意，又有多种（Poly）数学（Math）之意，双关，译者注）。

陶哲轩第一时间加入其中。他和高尔斯都清楚，并非所有数学难题都适合大规模协作，适合协作的难题需满足一个核心条件：能够拆解为大量可并行推进的子问题。将主难题拆分为多个独立小问题后，不同团队、不同研究者便可分头攻关，最终整合所有成果，拼凑出完整答案。但陶哲轩也预判到，博学者模式最大的挑战在于统筹管理：既要梳理整合各方观点，还要逐一核验所有推导内容的正确性。

博学者计划首个研究课题，是优化黑尔斯-朱厄特（Hales-Jewett）定理（该定理研究用两种颜色为网格单元格涂色时产生的规律）。数十位数学家在论坛留下数千条讨论内容，历经数月协作，团队成功推导出该涂色规律更精准的结论。同年秋季，团队以联合笔名 "D.H.J. 博学者" （D.H.J. Polymath）发布论文，这也是史上首篇依托大规模公开协作完成的数学论文。高尔斯的尝试大获成功，专业数学家与数学爱好者携手，顺利完成了一项数学证明。

此后十年间，博学者计划陆续开展了 15 个课题，其中部分由陶哲轩牵头，该项目也逐渐受到主流媒体关注。2011年10月29日，《华尔街日报》刊发题为《新一代爱因斯坦，必将是乐于分享的科学家》The New Einsteins Will Be Scientists Who Share的报道，称博学者计划开创了全新的解题范式。

证明辅助工具 Lean 能够协助数学家完成定理证明：既校验推导过程，也可自动完成部分证明步骤。

Lean �群中，章鱼表情逐渐成为大家表达喜悦的专属符号。

尽管博学者计划取得了开创性成果，但在陶哲轩看来，这一模式仍存在时代局限性。大规模协作带来思维碰撞的同时，出错概率也大幅提升，所有内容都需要专人逐一人工核验，审核环节成为整个项目的瓶颈，也让博学者计划难以长久运转。

陶哲轩真正追求的，是一套高效的全新科学研究模式。他意识到，单纯依靠论坛协作远远不够，想要实现理想，必须借助计算机自动核验成果，替代低效的人工审核。但在2010年代，这项技术尚不成熟，实现难度堪比载人登陆火星。

陶哲轩多年来一直关注计算机形式化数学证明领域，也知晓该领域为数不多的成功案例。但他同样清楚，彼时的形式化数学工具实操性极差，多数场景下，投入的时间与精力远大于实际收益。即便如此，他依旧看好这项技术的潜力。在全球顶尖数学家群体中，陶哲轩是少数主动拥抱新型数学研究工具的学者。

2022年7月，为深入了解计算机在数学研究中的应用，陶哲轩牵头组织了一场专题研讨会，并邀请凯文・巴扎德（Kevin Buzzard）担任联合组织者 —— 巴扎德是当时全球推广形式化数学最具影响力的学者。

详情参阅：

小乐数学科普：2022国际数学家大会一小时报告《数学形式主义的兴起》Kevin Buzzard 演讲全文

小乐数学科普：专访ICM 2022国际数学家大会一小时报告者Kevin Buzzard：计算机可以成为数学家吗？——译自量子杂志

参会之初，陶哲轩认为 Lean 是一套复杂的工具，至少需要数月时间才能上手。但在巴扎德的鼓励下，他决定亲自尝试。同时，他也认为自己应当以身做则：既然致力于推广计算机辅助证明，就必须亲身实践。

2023年10月9日，陶哲轩在社交平台发文：“我决定正式学习交互式证明系统 Lean4，过程中也会借助人工智能辅助操作。”

随后，他在数学领域知名问答平台 MathOverflow 上，挑选了一道关于麦克劳林（Maclaurin）不等式的问题，尝试用 Lean 完成形式化证明，以此作为实操练习。他先按照传统学术规范，手写了一份共计 10 页的标准证明文稿，随后着手将这份证明转化为 Lean 形式化代码。

起初，陶哲轩预估一周就能完成任务，但很快便发现手写数学证明与编写 Lean 代码存在巨大差异。他感慨道：证明中最难的推导环节，在 Lean 中反而容易实现；而那些看似浅显直白的结论，转化为代码时却要耗费大量精力。

举个简单例子：传统数学证明中，若已知三个数字均大于 1，便可直接得出 "三数之和不小于 3" 的结论，无需额外解释。但 Lean 不接受无依据的主观断言，陶哲轩不得不花费时间，在数学库（Mathlib）中查找对应的引理，以此佐证这个显而易见的结论。此外，传统数学书写无需严格界定数域，数字 "3" 既可以是自然数，也可以是整数、实数，无需特意区分。但在 Lean 中，每一个数字都必须明确所属数域。由于多处遗漏数域标注，他的代码反复编译失败。

耗时近一个月后，2023年11月6日，陶哲轩终于在博客评论区宣布：“我已成功将这篇论文的证明内容完整转化为 Lean4 形式化代码。” 尽管这份代码的编写质量并不理想，但他正式成为 Lean 社群的一员。

学习 Lean 的同时，陶哲轩依旧推进着多项常规研究课题。其中一项合作项目，搭档包括多年好友本・格林、蒂莫西・高尔斯，以及格林的学生、现任加州大学圣地亚哥分校教授弗雷迪・曼纳斯（Freddie Manners）。这是一支实力顶尖的团队：高尔斯与陶哲轩同为菲尔兹奖主，格林也是数论领域的权威学者。

四人的研究目标聚焦于和集（sumset）这一数学概念。简单来说，给定一组数字，将集合中每一对不同数字相加，所有求和结果构成的新集合，就是原集合的和集。

如果原始集合内的数字杂乱无章，其和集的规模会十分庞大。例如 10 个随机数字，对应的和集约包含 50 个数字；1000 个随机数字，和集数量可达 50 万个。但如果原始集合具备规律，和集规模会大幅缩小 —— 因为大量求和结果会重复出现，而和集仅保留不重复的数值。比如数字 1 至 10 构成的集合（典型的等差数列），其和集仅包含 17 个数字，远少于随机集合的 50 个。

1960年代，计算机科学家卡塔琳・马顿（Katalin Marton）提出一项猜想：若一个数字集合的和集规模极小，那么该集合中必然存在长等差数列。21 世纪初，陶哲轩、高尔斯与格林曾针对该猜想的优化版本 ——多项式弗赖曼 - 鲁扎（Freiman-Ruzsa）猜想（PFR猜想）开展研究，后续研究陷入停滞。2023年，陶哲轩、格林与曼纳斯重启该课题，计划结合曼纳斯深耕的概率论方法推进证明。

三人意识到，将这套概率论技巧与高尔斯过往的研究思路相结合，或许就能彻底破解该猜想。于是高尔斯也加入协作团队。2023年整个夏季，四人稳步推进研究，深秋时分终于完成完整证明。（详情参阅：小乐数学科普：数学的"A-Team"证明了加法和集合之间的关键联系——译自量子杂志）11月9日，也就是陶哲轩将首份 Lean 形式化代码上传至代码托管平台 GitHub 的三天后，四人联合论文正式发布在arXiv学术预印本平台https://arxiv.org/abs/2311.05762。

深耕 Lean 的陶哲轩顺势提议：团队可以尝试将这篇重磅论文完整形式化。这篇论文难度适中、影响力深远，且论文用到的基础定义大多已收录在 Mathlib 中，无需额外搭建底层内容，十分适合转化为 Lean 代码。

但格林、高尔斯与曼纳斯都不愿花费时间学习 Lean。于是陶哲轩决定独自牵头推进这项工作，他也预料到，以自己的影响力，很快会吸引众多志愿者加入。

2023年11月13日，陶哲轩在 Lean 专属交流群新建讨论频道并发文：“大家好，我计划启动一项项目，将我、高尔斯、格林、曼纳斯联合完成的多项式弗赖曼-鲁扎（PFR）猜想证明，完整转化为 Lean4 形式化代码。我会借助这个频道统筹进度，欢迎所有愿意参与的志愿者加入。”

这是博学者计划的全新升级版本：不再从零攻克新难题，而是对已有成熟证明进行形式化转化；全程由 Lean 自动核验内容正确性，彻底摆脱人工审核的负担。

消息发出次日，斯德哥尔摩大学博士生雅埃尔・迪利耶斯（Yaël Dillies）便为项目搭建整体框架，将整份证明拆解为 13 个模块。陶哲轩进一步细化任务，把每个模块拆分为多条引理与基础定义。传统数学论文中，一条辅助证明的引理通常长达 20 行，而此次项目中，他将引理压缩至 5 行，最大限度拆分任务，方便更多人分头贡献力量。

项目启动首周，志愿者们主要负责补充 Mathlib 中缺失的概率论基础内容，核心任务是完成香农熵（Shannon entropy，用于衡量数字集合等数据的无序程度与不确定性）的形式化定义。与此同时，团队也在摸索全新的协作模式。初期交流延续了博学者计划的自由讨论形式，陶哲轩梳理待办任务，众人自由建言献策。

11月22日，陶哲轩整理出 22 条待完成引理并发布：“大家可以自愿认领任意引理，在评论区留言即可。” 消息一出，报名者络绎不绝。伦敦几何与数论研究所博士生保罗・勒佐（Paul Lezeau）留言：“我认领均匀随机变量的熵相关引理。” 加州大学洛杉矶分校博士生艾伦・安德森（Aaron Anderson）则表示，愿意攻克一般纤维恒等式相关内容。

口口相传之下，越来越多数学家加入项目。11月底，陶哲轩几乎不再亲自编写代码，主要负责统筹分配任务。11月28日，他发文表示：“目前项目临近收尾，志愿者人手充足，我新增一项小任务，欢迎大家认领。”46 分钟后，学者金・莫里森（Kim Morrison）便反馈任务完成。陶哲轩惊叹道：“速度太快了！非常感谢！”

项目尚未收尾，Lean 社群便开始探讨其深远意义：有人认为，项目的高效推进，标志着数学证明形式化进入高速发展时代；也有人认为，这份成功主要依托陶哲轩的个人影响力。项目收尾阶段，陶哲轩总结道：“我本人编写的代码并不多。这也印证了一件事：数学家即便不精通 Lean 编程，只要能够清晰梳理引理、搭建证明框架，同样可以牵头开展形式化项目。”

乌得勒支大学数学家、Mathlib 项目负责人约翰・科梅林（Johan Commelin）随即留言，提出理性思考：“这个PFR项目的成功具备特殊性，很难直接复刻。正因课题关注度极高，才吸引了大量顶尖志愿者参与。” 他还指出了行业现实困境：在当前学术评价体系下，参与证明形式化项目，并不会成为青年学者求职、评职称的加分项。“数学界目前尚未明确形式化研究者的学术定位，这类工作在就业市场中也难以获得认可。” 对此，陶哲轩回应：“今后为相关学者撰写推荐信时，我会主动提及他们在本项目中的贡献。”

2024年，陶哲轩已然成为推广机器辅助数学的核心发声者。彼时，他已在美国总统科学技术顾问委员会任职三年，并担任生成式人工智能专项工作组联合主席。在2024年多场重要演讲中，他描绘了新一代数学协作模式：融合人类的原创思维、大语言模型的算力优势，以及形式化核验系统的严谨保障。

这份构想，源于他对当下人工智能能力的清醒认知。现有人工智能擅长解决数据充足、思路明确的常规问题，但面对数学前沿领域 —— 这类领域缺乏海量公开研究成果、难以搭建训练数据集，人工智能便会力不从心。在测试大语言模型的过程中，陶哲轩发现，这类工具就像过度自信的本科生：能够主动给出解题思路，却无法分辨观点的优劣对错。

但陶哲轩依旧找到了人工智能与数学结合的可行路径。他认为，人工智能短期内绝不会取代人类数学家，却十分适合拆解大型复杂数学难题：将主问题拆分为数千个简单子问题（这与博学者计划的思路不谋而合）。人工智能可批量攻克难度最低的子问题，并输出经过 Lean 核验的标准形式化证明；而人类数学家则聚焦攻克剩余的核心难题。2024年，陶哲轩四处宣讲这套研究模式。在多项式弗赖曼-鲁扎（PFR）猜想形式化项目成功后，他决定亲自牵头，落地这套全新研究体系，而他选定的首个课题，源自2023年偶然看到的一道趣味问题。

2023年7月，MathOverflow 上一名用户提出一道看似简单的谜题：以加法运算为例，加法满足交换律（x+y=y+x）、结合律（(x+y)+z=x+(y+z)）等基础代数法则。多数情况下，不同法则之间相互独立 —— 比如交换律无法推导出结合律。

这道谜题探讨两条特定代数法则之间的逻辑关系，很快便有网友给出解答。但各类代数法则之间的内在关联，深深勾起了陶哲轩的好奇心。他不再局限于解答零散谜题，而是着手梳理一张图谱，梳理所有代数法则之间的推导关系。梳理过程中他发现，这套逻辑体系远比想象中复杂。

他划定研究范围：仅分析运算次数恰好为四次的代数法则。经统计，这类法则共计 4694 条。任意两条法则之间，都存在 "能否相互推导" 的逻辑关系，总计需要验证 2200 万组逻辑推导。逐一完成所有验证（要么证明推导成立，要么举出反例推翻推导）后，就能完整厘清这 4694 条法则的全部关联。在陶哲轩看来，这个课题的规模，完美适配他构想的新一代数学研究模式。

陶哲轩将这个全新项目命名为等式理论（Equational Theories）https://teorth.github.io/equational_theories/，并于2024年9月25日在个人博客正式官宣。开篇他总结了传统大规模公开数学协作模式的诸多弊端，并直言：“Lean 这类证明辅助语言，有望彻底破解这些难题。”

项目启动后，陶哲轩与大批志愿者率先借助泛代数结构——原群（magma）开展测试。原群是简化版的算术结构，十分适合作为研究起点：若某条法则在原群中不成立，便不可能推导出其他更复杂的法则。志愿者们运用基础 Python 脚本，批量测试海量法则。短短数日，2200 万组逻辑推导中，超过 99% 都得到验证。

项目启动第二天（9月27日），陶哲轩发文感慨进度远超预期：“项目推进速度、协作规模都大大超出我的想象。仅仅 48 小时，绝大部分逻辑推导即将完成验证。此前为期三周的多项式弗赖曼-鲁扎猜想项目已算高效，而本次项目的推进速度更是创下新高。”

基础推导验证完毕后，志愿者们借助全自动定理证明器，结合人工推导，逐一攻克剩余难题。整个项目逐渐走向去中心化运转，许多研究进展甚至不再经过陶哲轩统筹。他对此评价道：“项目已实现自主运转，不少研究工作我都未能实时跟进，这正是我希望看到的状态。”

部分数学家认为这个课题新奇却略显冷门。全程关注项目进展的巴扎德表示，这是一场有趣的社会实验，只是课题本身的数学内容较为基础、风格另类，但他十分认可陶哲轩的创新思路。知名数学家约翰・贝兹（John Baez）则直言：“在我看来，这项工作纯粹是浪费时间。” 随后他又补充道，自己也曾用同样的看法看待大学橄榄球，但依旧有无数人乐在其中。

项目推进一个月后，2200 万组待验证逻辑推导仅剩 238 组；11月末，剩余数量缩减至 138 组。随着难题难度逐步提升，进度明显放缓。2025年伊始，仅剩下 30 组推导悬而未决，推进速度进一步下降。截至2025年3月底，团队卡在最后4组推导上，停滞数周。剩余难题过少，大量志愿者陆续退出，陶哲轩的项目更新频率也从每日播报，变为数周一更。

不过，彻底攻克全部 2200 万组推导，本就不是 "等式理论" 项目的核心目标。陶哲轩最初只是出于好奇，想要绘制出完整的代数法则关联图谱，如今除少数细节外，核心目标已然实现。更重要的是，在他眼中，这个项目是实验性数学新时代的试点工程，而这场试点无疑大获成功。（详情参阅陶哲轩原群等式定律——数学家群体合作大项目440天基本收官，就差临门一脚！）

陶哲轩认为，“等式理论” 项目拉开了实验性数学时代的序幕。他以物理学的发展历程类比数学：物理学也曾以理论研究为主，依靠独立学者或小型团队逐一攻克难题，和如今的数学研究模式高度相似。但随着技术革新，实验物理应运而生。欧洲核子研究中心的大型强子对撞机等大型实验装置，汇聚数百乃至数千名专业研究者协同作业，产出海量实验数据。实验物理并未取代理论物理，而是与之相辅相成，两类研究成果相互启发、彼此推进。

陶哲轩坚信，数学也将迎来同样的变革。全新的研究模式，必然会催生全新的数学发现。在志愿者逐条验证海量逻辑推导的过程中，团队意外发现了全新的数学概念 ——原群上同调。这一概念是群上同调的全新延伸，而群上同调是数学界研究已久的经典领域，主要探究群结构的拓展规律。陶哲轩特意请教该领域权威学者、此前并不看好项目的约翰・贝兹，对方坦言，从未见过这类全新构造。

这正是陶哲轩打造新项目的初衷。他并未指望 "等式理论" 能诞生颠覆性数学结论，而是希望借此验证一套全新数学研究体系的可行性。从这个角度来看，项目圆满达成目标。陶哲轩成功探索出数学研究的全新路径，而他也坚定地选择沿着这条新路继续前行。

本文节选自凯文・哈特内特著作《代码中的证明：一台真理机器如何重塑数学与AI人工智能》。该书由《量子图书》Quanta Books联合法勒（Farrar）、斯特劳斯（Straus）和吉鲁（Giroux）出版社出版，定于2026年6月9日正式发行，版权所有。

参考资料

https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

文章精选：

1.编程时代已终结！ClaudeCode创始人断言：编程就像发短信一样自然，首曝个人最新工作流：自创Sloop循环，单日PR达150！传统SaaS护城河崩掉