陶哲轩谈AI与形式化：数学研究的范式革命已经开始|定理|数学|数论|陶哲轩|黎曼

近日，Math Inc. 与知名数学家陶哲轩进行了一场深入对话。作为 2006 年菲尔兹奖得主，他近年来在形式化数学与 AI 辅助证明领域的探索引发了学界广泛关注。

从 2023 年底领导团队在三周内完成多项式 Freiman-Ruzsa 猜想（Polynomial Freiman-Ruzsa Conjecture，PFR）的 Lean 形式化验证，到 2024 年发起的“等式理论计划”（Equational Theories Project），陶哲轩正在身体力行地推动一场数学研究范式的变革。这次对话中，他坦诚地分享了自己对形式化工具、AI 技术以及数学未来的思考。

他的核心观点包括：

一、形式化正在改变数学写作和思维方式。Lean 等工具迫使数学家更清晰地定义概念、检验假设，能自动发现“你其实从没用过这个假设”——这有时带来真正的数学进展。

二、形式化让证明修改变得极其高效。PFR 猜想的形式化证明从 C=12 更新到 C=11，传统方式可能需要再花三周，但在 Lean 中只用了一天。

三、数学研究可以像软件工程一样分工协作。不是每个人都需要懂 Lean、懂数学、懂 GitHub——只需要重叠的技能组合。这将让更多“数学爱好者”参与前沿研究。

四、解析数论是自动化的理想目标。该领域约 70% 的工作是繁琐的常数计算和参数匹配，一旦形式化，就能像 Excel 一样自动更新——有人证明了新边界，整个领域的相关结果可在几分钟内同步更新。

五、形式化建立了新的信任基础设施。传统数学依赖“圈子”和声誉来判断结果可靠性；有了 Lean 验证，你可以使用素未谋面者的结果。

以下是对话全文。

问：你是从什么时候开始对机器辅助证明产生兴趣的？

陶哲轩：回顾整个职业生涯，我始终觉得我们做数学的方式缺少了某些东西。研究一个数学问题时，我们追求的是那个能解锁答案的精妙想法，但在抵达那个时刻之前，有大量琐碎的工作需要完成——文献综述、技术细节调整。你在另一篇论文里发现一个有价值的技巧，想应用到自己的问题上，却发现所有的输入条件都略有出入，于是不得不手工调整论证、反复计算。这些工作当然是有意义的，能帮助建立直觉，但很多时候纯粹是苦力活。我以前也尝试过写一些小型计算器来加速部分计算，但当时技术尚未成熟。

大约两年前，我们在 IPAM（Institute for Pure and Applied Mathematics，纯粹与应用数学研究所）举办了一场机器辅助证明的会议，我是组织者之一。在那里，我们接触到了各种前沿尝试，SAT 求解器、计算机辅助软件包、大语言模型等等。ChatGPT 刚刚问世，Lean 也在蓬勃发展。突然间，许多原本遥不可及的事情变得触手及极，整个领域正在经历某种觉醒。

Peter Scholze 刚刚完成了一个历时 18 个月的项目，用 Lean 形式化了他的一个重要定理：液态张量实验（Liquid Tensor Experiment）。一个定理，18 个月，20 余位协作者。这在当时已被视为重大突破，因为 20 世纪的形式化项目往往需要数十年才能完成。速度的提升部分归功于我们学会了使用软件工程的工具——GitHub、更智能的项目组织方式。

问：那次会议促使你开始学习 Lean？

陶哲轩：那次会议之后，我对 AI 和形式化都产生了浓厚兴趣，并确信这就是数学的未来方向。我开始接受采访，四处谈论这些想法。但到了某个节点，光说不练是不行的，必须真正动手。于是我开始学习 Lean，大约花了一个月时间。这个过程其实相当有趣，让我想起当年撰写本科实分析教材的经历——从自然数的构造讲起，把每一个细节都处理得完全严谨。使用 Lean 的感觉很像在玩电子游戏。Kevin Buzzard 曾说 Lean 是“世界上最好的电子游戏”，对某类人来说确实极易上瘾。

而在过去一年里，大语言模型的能力突飞猛进，已经能够自动形式化单个证明步骤，大幅减轻了形式化过程中的繁琐工作。现在甚至可以实时进行形式化，这打开了无数新的可能性。

问：我在学习形式化证明的过程中有一个深刻体会：我逐渐意识到自己其实从未真正学会清晰地思考数学论证。高等数学的证明中似乎存在某种约定俗成的模糊性。随着你越来越深入地接触形式化，你对自身数学认知的理解是否也发生了变化？

陶哲轩：确实有所改变，尤其体现在写论文的方式上。我现在能够察觉到那些“隐形假设”，那些我们习惯性地默认却从不明说的前提。你会更认真地思考：怎样定义一个概念才是最干净的？因为在 Lean 中，定义一个概念之后若想使用它，首先需要围绕这个概念建立一系列基本引理，也就是所谓的 API。

这些引理在论文中往往一笔带过，“显然这个概念是单调的”“显然它在并集下封闭”，但你确实应该证明它们。而如果定义方式不够恰当，形式化这些“显然”的陈述会花费两倍甚至五倍的时间。这种经历让我对如何改进自己的写作有了新的视角。坦白说，有时候我甚至会对合作者产生些许不满，因为他们还没有接触过这种思维方式，仍在沿用旧的非形式化风格。

Heather Macbeth 曾撰文讨论形式化和自动化如何催生一种新的证明写作风格。传统证明通常是线性的，从 A 推导到 B，你试图找到一条等式链或推理路径。但借助自动化工具，你可以换一种方式表达：这里有 10 个相关事实，要从 A 到达 B，可以用标准工具找出这些事实的恰当组合来完成任务。这个组合过程往往是技术性的、不太有趣的，比如某种线性代数运算之类。这是一种不同的证明风格，在某种意义上反而更易于阅读。对人类来说虽然更难手工验证，但你能更清晰地看到证明的输入和输出，而传统写法往往把这些信息隐藏了起来。

Peter Scholze 的经历也印证了这一点，他说过，形式化过程中获得的反馈实际上帮助他更清晰地思考了那个关键引理的具体细节，他认为是非常有益的智识活动。

问：你提出过一个广为流传的框架：数学学习的“前严谨、严谨、后严谨”三个阶段。这个框架如何与我们正在讨论的话题相关联？

陶哲轩：是的，我写了那篇传播甚广的文章，讨论学习数学的三个阶段。第一阶段是“前严谨”阶段：你还不真正理解什么是证明，但对什么可行、什么不可行有一些模糊的直觉。这大致是小学阶段的数学理解水平，有时直觉是对的，有时是错的，而你缺乏区分两者的能力。

第二阶段是“严谨”阶段：你被要求严格按照规范行事，每一步都必须正确无误。在这个阶段，人们往往会暂时失去直觉，因为全部注意力都集中在确保每个步骤完全正确上。但这个过程会帮助你清除所有错误的直觉，你能看到论证失败的精确反例，同时保留那些经受住严谨检验的好直觉。

第三阶段是“后严谨”阶段：你可以在形式化与非形式化之间自如切换。你能够用非形式化的方式论证，但现在是安全的，因为错误的直觉已被清除；而且你知道，必要时可以将其转换回严谨形式。反过来，你也能阅读一个严谨的论证，并将其翻译成直觉性的语言。

Lean 确实帮助我清理了直觉中一些错误或低效的思维模式。一个典型的低效习惯是：在教科书中陈述定理时，我们往往添加过多的假设。出于谨慎，为确保定理正确，我们会堆砌各种额外条件，集合非空、函数连续、参数为正等等。

理想情况下，我们应该对这些假设进行压力测试。而 Lean 提供的自动检查器恰好能做到这一点：当你形式化某个证明后，它会提示你“顺便说一句，你从未使用过这些假设”，有时这会带来真正的进展。人们可能长期存在某种思维定势，认为某个工具只能在特定条件下使用，但证明本身其实并不依赖那个条件，只是从未有人注意到。形式化让我们能够自动发现每个工具的自然适用范围，这非常有价值。

问：这个总结非常精到。我们一直在思考的一个问题是：软件工程和计算机科学中的深层洞见如何影响人们对数学认知和数学研究的理解。你之前提到形式化如何清晰化每个定理的假设和输出，本质上就是良好的软件工程实践。Dijkstra 有一整套关于前置条件和后置条件推理的理论；同样，随意传播各种可能的假设是软件工程中典型的反模式。

我特别想问的是：你在形式化过程中的“顿悟时刻”是什么？学习一门小众的学术编程语言显然需要跨越最初的门槛，但在什么时刻你意识到，将数学转化为软件的过程本身也能加速理解，甚至推动数学发现？对我而言，这个时刻出现在形式化连续统假设独立性证明的过程中：我陷入困境，所有源材料都存在问题，然后我发现可以通过开关某些关键假设，迅速获得比任何教科书都更深刻的理解。我好奇你有怎样的类似经历。

陶哲轩：有两个时刻给我留下了深刻印象。

第一个发生在形式化 PFR 猜想的证明时。这是加性组合学中的多项式 Freiman-Ruzsa 猜想。证明中有一个指数 C，最终等于 12，这是将证明各处的小常数组合起来得到的结果。我们花了三周时间写出蓝图，动员了 20 个人来形式化这个 C＝12 的证明，全部手工完成，那是在 AI 时代之前。后来有人在 arXiv 上发布了一篇短文，指出如果对源论文做 5 处修改，可以将 12 降到 11。有人问：我们要不要也形式化这个？我心想，形式化 C＝12 花了三周，C＝11 岂不是又要三周？

但实际情况是：你只需在 Lean 的最终陈述中将 12 改成 11，然后观察哪些代码行变红，它们不再被证明正当。你对照新的预印本，发现可以这样修复这 5 行使其编译通过；但修复之后，另外 10 行又变红了；于是你继续处理那些。一天之内，我们就完成了整个证明向 C＝11 的更新。形式化第一个结果确实繁琐，但一旦需要修改证明，它的效率远超传统方式，即便没有 AI。

第二个经历来自另一个项目“等式理论计划”。有人在形式化他人撰写的证明时在某一步卡住了，说：“我不知道怎么处理这一步。”我查看了那一行代码。虽然不理解整个证明，但我能理解那一行及其足够的上下文，于是告诉他：“你只需要这样修改这一行，就能使用那个工具了。”我可以给出非常原子化的诊断——如何修复一个 1,000 行代码中的问题，只需检查其中 3 行。

这是 Lean 的独特之处：形式化验证过的软件具有高度模块化的特性，其他软件难以企及。你可以进行真正原子化的讨论，只聚焦于代码中非常具体的几行，而无需理解其他部分发生了什么。

在传统数学中，这种交流只能与那些我完全熟悉的合作者进行。我们必须长期共事，达到能够理解彼此思维方式的精细程度，甚至能够接续对方的话。进入那种状态是美妙的，但我只与少数几位合作者建立了这样的默契。与新人合作时，你必须解释所有定义，还会产生各种误解。但有了 Lean，这一切障碍都消失了，因为你拥有对问题本质和解决方案的精确类型描述。

它以一种前所未有的方式将数学原子化了。

问：你是互联网数学协作的先驱之一，包括 Polymath 项目这种众包数学研究的模式。能否谈谈你对数学协作的理解在过去 20 年间是如何演变的？以及在这种高度模块化、有时甚至匿名的互动方式下，数学的未来会呈现怎样的面貌？另外，你几年前在 Notices of the AMS 上发表的文章中讨论了数学家角色的演变。我好奇，随着你组织这些形式化项目，你对自身角色的理解发生了怎样的变化，以及运营 Polymath 项目积累的经验如何与此相互作用？

陶哲轩：我一直感到想做的数学远超个人所能完成的范围，因此始终认为协作极具价值。我从合作者那里学到了很多，也从互联网上的随机交流中获益匪浅。我开始写博客源于一次偶然经历：有一次我在个人网页上发布了一个数学问题，并不指望有人回应。但那时已经有足够多的人关注我的页面，三天之内我就收到了关于这个问题来源的完整文献索引。现在这其实是一个简单的 ChatGPT 查询就能解决的问题，但在当时，这对我是革命性的。

后来 Tim Gowers 发起了 Polymath 项目，尝试众包数学研究，我非常投入。这与我的理念产生了共鸣。参与者越多，就越有可能产生那种任何单个专家都无法独自发现的意外联系。但这些项目始终存在瓶颈：当有一二十人贡献时，必须有人检查所有答案、确保整体连贯并撰写总结。这个人要么是我，要么是 Tim Gowers，要么是其他核心成员。这极其消耗精力，你就像星形网络的中心节点。

因此，虽然前景诱人，这种范式终究无法规模化。它确实促成了一些非常广泛的项目，参与者从数学的各个领域贡献联系，这些领域与项目的关联性是组织者事先完全没有预料到的。但我们缺乏验证的组织基础设施。而且当时我们是在博客或 wiki 上运营，而非像现在这样使用 GitHub。

形式化和 AI 真正实现的，是让具有不同技能组合的人能够无缝协作。在形式化项目中，并非每个人都需要精通 Lean，并非每个人都需要深谙数学，也并非每个人都需要熟悉 GitHub。你只需要一组具有重叠技能的人，每个人掌握其中一部分即可。这使得数学项目中真正的分工成为可能。

在传统数学项目中，你可能有一两位合作者，但即便是协作，每个人也必须承担所有工作：每个人都得理解数学、都得会写 LaTeX、都得能检查论证，每个环节每个人都要参与。而在真正的分工体系中，有专人管理项目、有专人负责质量保证，就像工业化生产和专业化分工那样。

软件工程早已想通了这一点。软件开发过去也是单枪匹马的黑客模式，但那种方式无法支撑大规模系统。企业级软件需要专精于不同领域的人协同工作。我预见数学研究也将越来越多地采用这种规模化、专业化的模式。当然，传统的手工艺式数学仍将存在并受到珍视，但我们将拥有这种高度互补的新方式。

问：这是否意味着你预见大多数职业数学家的角色将演变为这类工业化系统的架构师？

陶哲轩：我认为“数学家”的定义本身将会拓宽。会有擅长运营大型项目的人，他们是项目经理，懂得足够的数学和足够的 Lean 来把握高层面的进展，但未必能解决具体的技术细节；他们的核心能力在于协调大型项目。

会有一些人特别擅长形式化，或特别擅长使用新的 AI 工具，但未必是某个数学分支的领域专家。

人们可以更灵活地加入和离开项目。当然，你也可以选择更传统的方式，让小团队里每个人深度参与所有环节。我认为这仍然是做数学的重要方式之一。

关键在于我们有了选择。目前，许多热爱数学的人被排斥在数学研究之外，因为门槛太高了。如果你想参与前沿研究，你需要具备博士级别的数学素养，需要熟练使用 LaTeX，还需要确保写作不出任何差错。这对许多数学爱好者来说过于艰巨。而那些确实尝试参与的人，常常被当作民科打发，因为他们的技能组合存在太多缺口。但社会上确实存在强烈的需求：数学界需要类似“公民科学”的模式。

我现在深度参与一个叫做“Erdős 问题”的网站，它已经发展成一个社区，几十位不同数学教育背景的人在贡献各种工作。我们找到了模块化问题的方法：也许你无法解决整个问题，但你可以挖掘相关文献、建立与某个整数序列的联系、评论他人的证明、进行数值实验。有一批潜在的人渴望参与研究级别的数学，这些工具有望为他们打开大门。

问：到目前为止，我们讨论了你在形式化前沿的经验，以及协调大规模数学研究的经验。我想这是一个合适的时机来谈谈你正在推动的解析数论边界形式化项目。也许我们可以从一个简要说明开始，让普通读者理解为什么这个问题重要，以及它如何体现我们之前讨论的这些主题？

陶哲轩：让我提供一个思考框架。我倾向于将自动化视为人类思维的补充工具。使用计算机研究数学，最显而易见的方式是拿人类想攻克的最难问题，比如黎曼假设，让计算机去尝试。计算机在这类人类关注的问题上会取得一定进展，但我认为，至少在近期，它们在那些与人类偏好完全正交的方向上会更加成功。具体而言，那些涉及大量繁琐数值运算、需要筛选海量排列组合的工作，人类可能不喜欢做，而 AI 完全没有这种障碍。

在我所研究的方向之一的数论领域，有一个分支包含大量这类繁琐的计算工作，而迄今为止只有人类能完成。据我估计，思考一个解析数论问题时，至少 70% 的时间消耗在这种苦力活上。

我们拥有许多精妙的想法和工具，可以将一类关于数字、指数和或黎曼 zeta 函数的陈述转化为另一类我们关心的陈述。但这些工具都有各自的输入输出要求，你需要将它们恰当地串联起来。你可以在论文中找到这些工具，但每篇论文使用不同的符号体系，有时它们的假设条件与你的需求不完全匹配，于是你不得不拆解原始证明，构建自己的版本。

这涉及大量重复造轮子和参数调整的工作，而且容易出错。为了减轻痛苦，我们发明了一些变通方法。其中之一是声称“不关心常数”：与其写出“这里是常数 27，那里是常数 38”，我们统一用 C 表示，只说“这是某个常数”，不去计算具体数值。这减少了计算量，也在一定程度上防止错误。如果你在常数上犯了算术错误，但结论仍然表述为“存在常数 C 使得 ……”，就不会造成严重后果。

但代价是：我们数论中的许多结果不是显式的。你可能证明了“每个足够大的奇数都是三个素数之和”，但“足够大”究竟是多大？大于某个 C，而这个 C 具体是多少，我没有算，太麻烦了。

因此，只有一小部分被称为“显式数论”的领域会精确计算所有常数。这类工作更加繁琐，愿意从事的人更少，相关论文读起来也不愉快，这不是作者的问题，而是内容本身的性质决定的，大量显式计算本就不具有文学性。

但我认为这恰恰是自动化的理想目标。如果我们能建立某种流水线，将这些显式论文形式化，其中的核心思想和输入已经相当清晰，主要挑战在于匹配众多略有差异的工具、对齐所有参数，我相信这完全在当前技术的能力范围之内。在此基础上，我们还可以利用 AI 或机器学习来寻找最优的串联方式。

这将为审视整个领域创造全新的视角。例如，如果有人证明了关于黎曼 zeta 函数的新边界，我们希望能将其“投入”一个包含 100 个形式化定理的库中，像 Excel 表格一样自动更新：改变一个单元格，所有相关单元格随之刷新。

我们可以拥有一个动态的、实时更新的领域知识库，而非那些写死指数的静态论文。目前，每当某个结果改进，就需要手工重写现有论文来计算最新边界。对于任何给定的结果，这种更新大约每 10 年才进行一次。但如果有了正确的工具，这可以在几分钟内完成。

问：你是说这本质上是一个软件问题。这或许类似于早期程序员看待汇编语言的方式——繁琐，子程序隐藏在代码中，称不上文学，但一旦能够在更高抽象层次上推理 ……

陶哲轩：正是如此。现代软件原则上是可互操作的：你可以调用其他模块，有标准化的接口让软件工具相互通信，你可以构建大规模的复杂生态系统。当然，也因此会有更多 bug。但有了 Lean，我们有望以一种无 bug 的方式实现大量研究者之间的互操作。这是目前根本不存在的东西。

问：你认为数论或其他领域有多大比例的工作是由这类繁琐活动构成的？

陶哲轩：这个比例很难精确量化，而且我认为影响是间接的。正因为存在这些繁琐的计算，我们实际上会下意识地调整研究方向来规避它们。当一条思路开始变得计算量巨大、错综复杂时，我们往往会绕道而行，转向其他问题。所以如果只看论文中呈现的内容，繁琐工作的比例似乎并不高，但那是因为我们一直在绕开路上的坑洞。真正的代价不在于“我们花了多少时间做苦力”，而在于“我们因为不想做苦力而错过了多少机会”。

我相信当这些工具成熟之后，我们将改变做数学的方式。遇到大规模计算，我们会直接用技术工具去攻克它，而不是绕路回避。我们将能够突破那些现在几乎是本能般回避的障碍。所以表面的百分比看起来不高，但如果从错失机会的角度衡量，代价是巨大的。

问：你之前提到一个主要瓶颈是找到合适的合作者并与他们充分交流、共享思维状态。就目前人们研究显式解析数论边界的方式而言，有多大比例的时间被困在沟通结果、或在人类专家之间进行这种“分布式计算”以传播边界？如果你的愿景实现，该领域的研究可以加速多少倍？

陶哲轩：首先存在信任问题。这类计算中，如果某处出现一个错误步骤，整个计算就作废了。所以你必须知道谁是可靠的作者、谁不是。这是隐性信息，我们不会发布“不可靠作者名单”。因此，你必须了解这个社区，知道该向谁请教。如果某个结果不完全在文献中，但你可以问某位专家，对方会告诉你“对，只需要这样修改就行”。这里的瓶颈在于：你必须身处这个圈子，认识所有关键人物，才能在这个领域有效地工作。

我认为一旦有了形式化带来的信任保障，这个领域就可以更大程度地开放。你可以使用素未谋面者的结果，只要它经过 Lean 验证。这将解除大量工作的阻塞。

问：你提到了信任这个概念。一个研究者在某个领域持续工作，随着时间推移积累声誉和信任。一个真正激发我对形式化和数学基础兴趣的故事是沃沃斯基（Vladimir Voevodsky）的经历。他建立了非凡的声誉，证明了一系列惊人的结果，但在 90 年代末发表的一篇论文中，他大约 10 年后才发现存在一个关键错误。他由此认识到，所有人信任他只是因为他有辉煌的 track record，但这并不能真正保证正确性。