陶哲轩，AI人工智能走进数学领域的先行者Kevin Hartnett

助自动化证明校验工具，一道数学难题可被拆解为多个小模块（chunks），逐一攻克后再整合起来，且能确保每一个推导环节准确无误。在部分学者看来，这预示着数学研究即将迈入全新阶段。

诸如Lean这类自动化证明校验工具，能够为数学证明的严谨性提供绝对保障。

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

凯文・哈特内特（ Kevin Hartnett ）

陶哲轩向来乐于接纳非主流的全新理念。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 能够协助数学家完成定理证明：既校验推导过程，也可自动完成部分证明步骤。

数学库（Mathlib）

以 Lean 语言编写的数学知识库，全球数学家持续为其补充内容。数学家搭建证明整体框架，梳理推导步骤。

指令集（Tactics，策略集）

数学库中内置各类程序指令，可自动执行证明步骤；经过校验的定理会同步录入数学库。

核心内核（Kernel）

依靠固定规则逐行核验证明逻辑的正确性。

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

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

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

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