陶哲轩：AI让数学进入“工业化”时代

很多人提到数学研究，脑子里浮现的还是那个画面：一个人，一块白板，来回踱步，等灵感突然降临。

但当今世界最伟大的数学家之一、菲尔兹奖得主陶哲轩却告诉我们：这种“手工业时代”的数学研究模式正处于崩溃边缘，一场由 AI 和形式化证明语言（如 Lean）引领的“工业革命”已经悄然开启。

这一洞察来自陶哲轩最近的一次访谈：

在访谈中，陶哲轩指出，数学研究中存在大量的重复性劳动，如查阅文献、调整他人论文中的参数以及繁琐的计算。通过 LLM 辅助的自动形式化（Auto-formalization），这些琐碎的工作正逐渐变得轻松。

与此同时，Lean 等形式化证明语言与 AI 的深度融合正在改变数学协作的本质。形式化并不只是“把证明写得更严格”，而是把数学拆成了可以独立验证的原子步骤。这种原子化让分布式科研第一次变得可行。

陶哲轩预见到，数学界将出现类似软件工程的分工模式。未来的数学家可能扮演“架构师”或项目经理的角色，领导大型协作项目。这种模块化的研究方式可能允许“公民数学家”（非专业领域专家但具备某些技能的人）参与到前沿研究中，降低进入门槛。如此一来，数学研究的进展或显著加速。

参与访谈的另外两位数学家分别是前 OpenAI 研究科学家、Morph Labs 创始人 Jesse Han，以及斯坦福大学助理教授 Jared Duker Lichtman。

以下是机器之心整理的访谈记录。

从几十年到 18 个月

数学研究正被加速

陶哲轩： 说实话，在我整个学术生涯中，我一直觉得我们做数学的方式少了点什么。我们在研究一个数学问题时，总想找到那个能打开问题大门的精妙想法。但在那之前，有大量枯燥的苦力活。比如文献综述，比如你在别人论文里看到一个技巧想用到自己的问题上，但所有的输入条件都有点不一样，你就得手动调整所有的论证。还有那些计算 —— 它们确实有用，能帮你建立直觉，但很多时候就是硬磨，不停地算啊算。我以前也试过写一些小程序来加速某些计算，但那时候技术还不成熟。

大概两年前，就在 IPAM（纯粹与应用数学研究所）这里，我们办了一个机器辅助证明的会议，我是组织者之一。在那次会议上，我们接触到了各种各样的尝试 ——SAT 求解器、计算机辅助软件包、大语言模型。ChatGPT 刚问世，还有 Lean。那是一个令人兴奋的世界，你突然发现很多事情变得可能了，而且正在发生。比如 Peter Scholze 刚完成了一个长达 18 个月的项目，把他的一个重要定理形式化了 ——

Jared Duker Lichtman：液态张量实验。

陶哲轩： 对，液态张量实验。这是个大工程，一个定理花了 18 个月。但这已经被认为是巨大的突破了，因为 20 世纪的那些形式化项目，动辄要花几十年才能完成。所以这本身就是一个巨大的提速，部分原因是我们已经学会了如何使用软件工程的那些工具，比如 GitHub，以及更智能地组织这些项目。从那以后，我对 AI 和形式化都产生了浓厚的兴趣 ——

Jared Duker Lichtman： 就是因为那次会议。

陶哲轩： 对，没错。我开始相信这就是数学的未来，也开始接受一些采访谈这个话题。但到了某个时候，你不能光说不练，得真正动手。所以我就去学了 Lean，花了大概一个月，但其实挺好玩的。这让我想起了写本科分析教材的经历 —— 真的是从基础开始，把每一步都做到完全严格。感觉就像在玩电子游戏。我记得 Kevin Buzzard 说过，Lean 是世界上最好玩的电子游戏，大概是这个意思。

Jared Duker Lichtman： 让人完全上瘾。

陶哲轩： 对某类人来说确实非常上瘾。而在过去一年里，大语言模型追上来了，它们现在可以自动形式化单个证明步骤，真正开始减轻形式化过程中的苦力活，甚至到了可以实时完成的程度。这打开了无数的可能性。

形式化正在改变数学思维

把含混经验转化为可检验的结构

Jesse Han： 我第一次接触 Kevin Buzzard，是 2017 年他在 MSRI（美国数学科学研究所）教自守形式那门课的时候。几年后我跟他聊天，他说他当时根本没在关注那门课的内容，因为那个夏天他正在自学 Lean—— 在 Tom Hales 在第一届大型证明会议上告诉大家 Lean 将是未来之后。

我自己在第一次学习形式化证明的时候，有一个体会是：我慢慢意识到，其实我从来没有真正学会清晰地思考数学论证。高等数学的证明里有一种普遍的，或者说文化性的混乱感。我很好奇，当你越来越深入地去预判如何形式化证明时，你对自己数学思维的认知有什么变化？

陶哲轩： 确实有一些变化，改变了我写论文的方式。我现在能看到那些“隐形假设”—— 那些我们习惯性地默认成立的东西。你会更认真地思考：怎样才是最干净的定义方式？因为在 Lean 里，当你定义一个概念并想使用它时，你必须先建立一堆琐碎的引理，就是所谓的 API，围绕着每个概念。这些东西在论文里往往是“显然这个概念是单调的”“显然它在某种运算下封闭”，但你其实应该证明它们。而且你会发现，如果定义得不够好，形式化这些“琐碎”命题要花两倍甚至五倍的时间。所以这让我学会了如何精简自己的写作。有时候我会对合作者有点不耐烦，因为有些人没有这个视角，还在用老式的非形式化风格写东西。

Heather Macbeth 写过一篇文章，讲形式化和自动化如何催生了一种新的证明写作风格。传统的证明通常是线性的，从 A 到 B，一步一步推，比如一串等式。但有了自动化工具，你可以说：这里有 10 个相关的事实，用一个标准工具来找出这 10 个事实的正确组合就能完成证明。而这个组合往往很无聊，没什么意思 —— 你知道某种线性代数之类的东西能从这些事实得出结论。这是一种不同的证明写作风格，某种意义上反而更容易读懂。对人类来说更难验证，但你能更清楚地看到一个证明的输入和输出，而传统写法往往把这些藏起来了。

Jared Duker Lichtman：Peter Scholze 的情况也是这样，他说过，在形式化过程中获得反馈，实际上让他对某个关键引理的细节思考得更清楚了，他觉得这是一个非常有价值的过程。你有一个很棒的框架 —— 前严谨阶段、严谨阶段、后严谨阶段。这个框架怎么融入我们现在讨论的话题？

陶哲轩：对，我写过一篇传播很广的文章，讲学习数学的三个阶段。第一个是前严谨阶段，你并不真正知道什么是证明，但对什么行得通、什么行不通有一些模糊的直觉。这通常是小学阶段对数学的理解方式。有时候你的直觉是对的，有时候是错的，但你没有办法分辨哪个是哪个。

然后是严谨阶段，你被迫完全按照规矩来，每一步都要做得准确无误。但在这个阶段，你往往会失去直觉，因为你全部的注意力都在确保每一步都正确。不过这有助于清除你所有错误的直觉，因为你能看到精确的反例，知道论证在哪里失败了。而所有好的直觉 —— 那些与严谨推理一致的 —— 都会保留下来。

然后是后严谨阶段，你可以在两种模式之间自由切换。你可以非形式化地论证，但现在是安全的，因为你已经清除了所有错误的直觉。你知道如果需要的话，可以把它转换回严谨的形式。反过来，你也可以读一个严谨的论证，然后把它转换成直觉性的语言。

Lean 确实帮我清理了一些思维中低效或错误的习惯。一个很常见的低效问题是：当你在教科书里陈述一个定理时，往往会加入太多假设。你有点过于保守，想确保证明是对的，就加了一堆额外条件 —— 这个非空、那个连续、这个为正之类的。

Jared Duker Lichtman：你会想去对这些假设进行压力测试。

陶哲轩：对。但其实还有自动化的 linter 工具，当你在 Lean 里形式化某个东西，证明结束后它会说：“顺便提一下，你从来没用过这个假设。”然后你就会想：“哦，确实，我其实根本不需要正性条件。”文献里确实有过这样的真正突破：人们心里有个思维定式，觉得某个工具只能用在比如正数的情况下，但其实证明在没有正性条件的情况下照样成立，只是没人注意到。形式化能让你自动发现每个工具的自然适用范围。这已经非常有用了。

Jesse Han：这个说法很精辟。我们花了很多时间思考一个问题：来自软件工程和计算机科学的深度洞见，如何影响人们对数学认知和数学研究的思考方式。你刚才说的形式化如何让我们更清楚地理解每个定理的假设和输出，这其实就是良好的软件工程实践。Dijkstra 就专门讲过，人们应该更多地去推理前置条件和后置条件。同样的道理，数学家习惯在定理里堆一堆可能用不上的假设，这在软件工程里是典型的反模式 —— 一种公认的坏习惯。

两个顿悟时刻

形式化正在改变数学领域协作方式

Jesse Han：我特别想问你的是：你在形式化过程中的“顿悟时刻”是什么？显然一开始有很高的启动门槛，你得学习所有这些关于这门小众学术编程语言的晦涩知识。但是，在哪个时刻你意识到，把数学变成软件这个过程，不仅仅是翻译，还能加速你的理解，加速数学发现的过程？

对我来说，是在形式化连续统假设的独立性时。有一个时刻我完全迷失了，所有的参考资料都是错的，但我发现可以打开或关闭某些关键假设，然后很快就获得了比任何教科书都深得多的理解。我很好奇你有没有类似的经历。

陶哲轩：有，我有两个印象特别深刻的时刻。

第一个是我在形式化一个和合作者一起证明的定理，叫 PFR 猜想 —— 多项式 Freiman-Ruzsa 猜想。结论里有一个指数常数，我们当时证明的是：存在一个常数，使得某个性质成立，而这个常数最后算出来是 12。原因并不神秘，只是把证明中所有零零碎碎的小常数一路累积下来，最后自然就变成了 12。

我们花了大概三周时间，把这个“C 等于 12”的结论完整形式化成 Lean 代码。那是一个完全没有 AI 的年代，整整 20 个人，全靠手工，是一次非常浩大的工程。

后来，有人往 arXiv 上放了一个很短的预印本，说如果你回到原始论文，只要做五个小澳动，就可以把这个 12 降到 11。于是大家就开始讨论：那我们要不要把 C 等于 11 也形式化一遍？问题在于，C 等于 12 已经花了我们三周时间，那再来一遍岂不是又是三周？

实际情况并不完全是这样，但直觉上你几乎只是把最终定理里的 12 改成 11。然后你会发现，大概有五行代码变红了，也就是证明不再成立了。但你去看那篇新的预印本，就会发现，哦，这五行我知道该怎么改。结果一改，这五行是好了，又有另外十行变红了。于是你再回去改那十行。就这样来回几次，我们在一天之内就把整个证明更新成了 C 等于 11。

所以，形式化确实很繁琐，尤其是第一次把一个结果完整写出来的时候。但一旦你想修改一个已有的证明，它就比传统数学方式好得多。这是我第一个非常深刻的体会。

第二个经历来自一个名为 Equation of Theories 的项目，然后对一项研究进行形式化时，有一次很深的体会。当时有人在把另一位作者写的证明形式化，结果卡在了某一步。我当时也并不了解整个证明的全貌，甚至可以说完全不理解整体结构，但我盯着那一行代码看了一会儿，发现我其实能理解这一行在做什么。

我能够理解足够多的上下文，从而指出：你这里其实只需要复制并稍微修改这一行，让它在类型上匹配，这样就能调用这个工具了。

也就是说，我只通过检查一千多行代码中的三行，就给出了一个非常原子级（atomic）的诊断，精确地指出了这个证明该如何修复。

我认为这正是 Lean，乃至形式化验证软件的一大特点：它具有一种高度模块化的结构，这是很多其他软件甚至传统数学中并不具备的。你可以围绕某一行、某一个非常具体的局部问题展开极其精细的讨论，而完全不需要理解系统的其余部分。

而在传统数学中，只有在与你长期合作、彼此已经在思维方式上高度对齐的情况下，才能做到这一点。那种状态下，你们几乎可以在极其细微的层面上互相理解，甚至补全对方的句子。

通常情况下，当你和一个尚未在思维方式上充分同步的人讨论数学问题时，是很难进行这种粒度如此之细的交流的。

所以你确实可以进入那种高度专注、默契协作的状态，那种感觉非常好。但现实是，能让我进入这种状态的合作者其实只有少数。更多时候，合作中充满了翻译成本：你需要反复澄清定义、解释背景，也不可避免地会出现各种误解。

而在 Lean 中，这些问题在很大程度上都会消失。因为你面对的是一个对问题和修复方式都有着精确定义的类型描述。问题是什么、哪里不匹配、该如何修复，都被明确地写进了系统里。Lean 以一种此前从未有过的方式，把数学原子化了 —— 这是其他做数学的方法所不具备的。

数学进入“工业化”时代

数学家也可以是架构师

Jared Duker Lichtman：顺着这个话题再往前想，其实也很有意思：我们正在用一种全新的方式来使用数学。你经历过互联网的兴起，也算是较早参与并推动了类似 Polymath （博学者项目）这种协作式研究项目的人之一。也许你可以谈谈，你对协作的直觉是如何形成的？在过去大约二十年的时间里，这种协作方式是如何演化的？

以及展望未来，在一种高度模块化的交互模式下，有时甚至是匿名的协作中，数学研究可能会呈现出怎样的新形态？

Jesse Han：我想再补充一点。你在几年前发表于《Notices of the American Mathematical Society》的一篇文章里，提到过一个非常有意思的观点：你如何看待数学家角色的演变。

我也很想听你进一步展开这一点，因为这和我们刚才讨论的内容高度相关，比如，当你开始主导、协调这些形式化项目时，你是否也感受到自己角色的变化？以及你在组织 Polymath 项目过程中积累的经验，又是如何与这种变化发生交汇、相互影响的？

陶哲轩：我一直都有一种很强烈的感觉：我想做的数学，远远超过了一个人所能完成的量。因此，我始终觉得合作极其高效、也极其重要。我从合著者身上学到了很多，同样也从互联网上一些看似偶然的交流中学到了很多。

举个例子，我最早开始写博客，其实源于一次非常偶然的经历。有一次，我在自己的网页上随手贴了一个数学问题，并没有期待会有人回应。但当时已经有不少人会浏览我的页面，结果在短短三天之内，就有人给了我一个非常完整的参考说明，直接指出这个问题最早的来源。放在今天，这可能只需要一次简单的 ChatGPT 查询就能得到答案，但在当时，这对我来说是一种颠覆性的体验。

后来，英国数学家 Timothy Gowers 提出了 Polymath 项目，希望通过众包的方式来做数学研究，而我也非常享受参与其中。这种想法和我的直觉高度契合：数学中存在着大量潜在的联系，参与的人越多，就越有可能产生那些偶然的连接，这些连接往往是任何单一专家、无论多么资深，都很难凭一己之力发现的。

但与此同时，这种协作方式始终存在一个明显的瓶颈。

在 Polymath 项目中，当同时有十几、二十个人参与贡献时，总需要有人来逐条检查这些想法，确保逻辑上一致，并把零散的讨论整理成一个连贯、可读的整体。这个工作通常由我、Timothy Gowers，或者其他少数人来承担，而这件事实际上是非常耗费精力的。

Jared Duker Lichtman：原本看似去中心化的群体协作，最终还是回到了一个核心人物 + 众多贡献者的老模式。

陶哲轩：对，这种模式虽然很有潜力，但并没有真正实现规模化。不过，它确实促成了一些非常宏大的研究项目：来自数学中完全不同方向的人，会因为偶然的灵感，贡献出大量有价值的线索。很多时候，项目的组织者事先根本不知道这些人彼此之间存在任何关联，但他们提供的想法却是相关且有用的。

问题在于，当时我们并没有完善的组织与验证基础设施。而且那时我们主要是通过博客和 Wiki 来运作项目，而不是像今天这样使用 GitHub 这类更成熟的协作平台。

也正是在这里，形式化工具和 AI 展现出了另一项关键能力：它们真正实现了不同技能背景人群之间的无缝协作。在一个形式化项目中，并不是每个人都需要懂 Lean，也不是每个人都需要精通数学，更不是每个人都要熟悉 GitHub。你只需要一个技能集合彼此有重叠的群体：每个关键环节都有一部分人能够胜任，整体就能顺利推进。

这也使得数学研究第一次真正具备了分工协作的可能性。

在传统数学研究中，无论是单人还是合作，参与者几乎都需要什么都懂：既要理解全部数学内容，又要会写 LaTeX、检查推导、整理论文，每个人都要覆盖所有环节。而在真正意义上的分工体系中，就像工业化生产一样，会有人负责项目管理，有人负责质量验证，有人专注于具体技术细节。

软件工程其实早就完成了这种转变。早期的软件开发也是一个人包办一切，但这种方式无法扩展；一旦进入企业级开发，就必须依赖高度专业化的角色分工。

因此，我确实预见到一种趋势：在规模化、工业化的条件下生产数学成果，并且伴随着清晰的专业分工。当然，传统的、手工式的数学研究依然会存在，也依然会被高度珍视；只是未来会出现一种与之互补的、全新的数学生产方式。

Jesse Han：那么，这是否意味着你预见到，大多数职业数学家的角色将会演变为这些工业化数学体系的架构师？

陶哲轩：我认为，数学家的定义本身会被拓宽。未来会出现一类人，他们擅长运作和管理大型项目，就像大型工程中的项目负责人一样。这些大型项目的管理者会掌握足够多的数学和 Lean 知识，能够在宏观层面理解项目在做什么，但他们未必擅长定位和修复某一条具体的形式化问题。尽管如此，他们能够协调复杂项目的推进，而这本身就是一种非常重要的能力。

同时，也会有一些人，他们可能并不是某个数学领域的专家，但非常擅长形式化工作，或者非常善于使用新的 AI 工具。这些能力本身同样有价值。

在这样的体系中，人们可以更自由地加入或离开项目，协作将变得更加流动。当然，也仍然会存在更传统的研究方式：由一个规模较小的团队组成，所有人都深度参与项目的每一个环节。这种方式依然非常重要，也不会消失。关键在于，我们终于拥有了多种选择。

在当前体系下，许多真正热爱数学的人被挡在数学研究之外，只是因为门槛太高了。如果你想参与前沿研究，就必须掌握博士阶段水平的数学；你还得会用 LaTeX；得知道如何写作、如何避免任何细节错误…… 这些要求叠加在一起，对很多人来说极具威慑性，进入门槛过高。

即便成功进入这一体系的人，也常常因为自身技能结构不完整而被忽视或边缘化。但未来并不必然如此，随着工具、形式化和协作方式的变化，这种状况有可能被根本性地改变。

Jared Duker Lichtman：在门槛被工具和协作机制降低之后，数学研究不再只属于少数职业数学家，而可以像公民科学一样，吸纳大量具有兴趣和部分技能的普通参与者。

陶哲轩：是的，我们其实已经在看到这种趋势了。比如我自己就深度参与过一个数学问题网站。它逐渐发展成了一个社区，聚集了几十位数学背景和受教育程度各不相同的参与者，大家各自贡献一些小而具体的内容。

我们学会了把一个问题模块化拆解：也许你没法完整地解决这个问题，但你可以帮忙查找相关参考文献；或者把问题和某个整数序列联系起来；或者评论、改进他人的证明；又或者做一些数值实验和计算。

正是通过这种方式，很多人都能在自己能力范围内参与进来。

而现实中，确实存在着一个非常庞大的群体，他们渴望参与研究级别的数学工作，只是过去缺乏合适的入口和工具。我希望，也相信，这些新的工具和协作方式，能够真正释放出这股力量。

AI 应该先帮数学家“干脏活”

Jesse Han：到目前为止，我们已经谈了很多内容：一方面是你在形式化数学前沿工作的经验，另一方面是你在协调大规模协作项目、加速数学研究方面的实践。而我觉得，正好在这两者的交汇点上，是一个非常合适的时机，来谈谈你目前特别投入、也非常兴奋推动的一个项目，解析数论中数学界限（Bounds）的形式化证明。

或许我们可以从一个简要的介绍开始：面向非专业读者，能否先解释一下 —— 为什么这个问题本身如此重要？以及它在某种程度上，如何成为我们刚才讨论过的那些问题（协作、形式化、规模化研究）的一个缩影或体现？

陶哲轩：我想先从一个更宏观的角度来讲。我一直认为，自动化本质上是对人类思维的补充工具。

最直观的一种思路是：把人类最想解决、也最困难的数学问题 —— 比如像黎曼猜想这样的重大猜想，直接交给计算机，让它们来尝试解决。计算机在这些问题上确实可能取得一定进展，但我认为，在可预见的未来，它们更有可能在另一类完全不同的任务上发挥巨大优势。

这些任务往往与人类真正擅长、或乐于从事的工作是正交的，尤其是那些需要进行大量枯燥的数值计算、枚举海量可能性、反复筛选组合情况的工作。这类任务人类通常并不享受，甚至极易出错，但对 AI 和计算机来说却并不构成障碍。

以我所从事的领域之一解析数论为例，这里就存在一个非常典型的困难：其中有大量极其繁琐、细碎的组合性计算工作，长期以来几乎只能由人类亲自完成，而这正是自动化和 AI 最有潜力介入、并发挥巨大价值的地方。

Jared Duker Lichtman：对我个人来说，在思考一个解析数论问题时，至少有 70% 的时间，都花在这种繁琐、机械性的工作上。

陶哲轩：是的，我认为我们其实已经掌握了很多非常精巧的思想和工具，可以把关于数字的一类陈述，或者关于和的展开、各种算术函数等内容，转化为我们真正关心的另一类陈述。解析数论中正是依靠这些工具在不同表述之间来回转换。

但问题在于，这些工具都有各自的输入和输出条件，而真正做研究时，你需要把它们一环一环地串联起来。相关的工具和结果分散在不同的论文中，每篇论文使用的记号体系都不一样，假设条件也往往和你手头的问题并不完全匹配。于是你不得不重新拆解原有证明，根据自己的需求重写一套版本。

在这个过程中，就会产生大量的重复劳动：反复调整参数、对齐条件、重建推导链条，而且非常容易出错。

为了让事情稍微不那么痛苦，我们发展出了一些权宜之计。其中一个最常见的做法是：不去关心具体常数。比如这里原本是 27，那里是 38，我们干脆都记成一个统一的常数 C，只说明存在某个常数，而不去计算它的具体数值。这样可以显著减少计算量，也能在一定程度上避免错误，即便你在常数上算错了，只要结论仍然成立，通常也不会造成严重后果。

但这种做法是有代价的。它导致解析数论中的很多结果都是非显式的。比如你可能证明了：所有足够大的奇数都可以表示为三个素数之和，但足够大究竟是多大？这个常数 C 到底是多少？我们并没有算出来，说白了，是懒得算。

因此，真正去显式计算所有常数的解析数论研究，只占整个领域中非常小的一部分。这类工作极其繁琐、计算量巨大，做的人很少，论文也往往不太好理解。这并不是作者水平的问题，而是因为研究内容本身就充斥着大量细碎、明确的计算过程，几乎没有那种直观的结构美感可言。

说实话，这种研究并不好理解。但我认为，这恰恰是自动化最理想的应用场景之一。如果我们能够搭建一条流水线，把这些显式型的论文纳入进来，其中的思想和工具本身其实已经相当成熟，真正困难的只是把大量彼此略微不兼容的工具拼接在一起，并把所有参数对齐，那么，用现有的方法就完全有可能在规模化条件下完成这些形式化工作。

在此基础上，我们甚至可以引入 AI 或机器学习，去探索这些工具链的最优组合方式。这将为整个领域打开许多全新的观察视角。

举个具体的例子：如果有人在某个算术函数上证明了一个新的界，我们希望能把这个结果直接丢进一个已经形式化好的、包含上百条定理的系统中，然后像操作 Excel 表格一样自动更新，改动一格，所有依赖它的结果都会自动刷新。

这样一来，我们就可以拥有一个持续演化、动态更新的领域最前沿状态，而不再是那些写死了指数和常数的论文。现在的做法是：每当某个关键结果被改进，研究者往往需要重写整篇论文，重新推导所有相关界限，才能弄清楚最新的最好结果是什么。而这类更新，通常十年才发生一次；但如果工具链足够成熟，这些工作完全可以在几分钟内完成。

Jesse Han：所以你的意思是，这本质上是一个软件问题，对吗？就像早期编程时代，人们看待汇编语言时那样，它非常繁琐，到处都是子程序，逻辑隐藏在代码细节里，既不直观，也谈不上可读性。但一旦能够在更高层次上对这些内容进行抽象和推理，情况就会完全不同。

陶哲轩：可以这么理解。而且在现代软件工程中，原则上一切都是可以互操作的。你可以调用别人的子程序，不同工具之间有标准化的接口和格式，它们能够彼此通信，从而构建起极其复杂、庞大的软件生态系统。

当然，这样的系统也会带来一个问题：正是因为系统复杂、组件众多，软件中不可避免会出现各种错误。

但在数学形式化这件事上，像 Lean 这样的工具，至少在理论上，让我们有机会构建一种尽可能无 bug 的协作体系。通过形式化验证，你可以希望、甚至确信这些由大量研究者共同构建的成果是相互兼容、逻辑一致的。而这正是我们目前在数学研究中所缺失的东西：一种真正可靠、可互操作、可规模化扩展的基础设施。

当新工具出现

数学的研究路径会整体改写吗？

Jared Duker Lichtman：那么你是否愿意做一个大致的判断或推测：在数论，乃至其他数学领域中，有多大比例的工作其实是由这些相对枯燥、机械性的劳动构成的？如果这种工作负担的比例发生改变，是否可能由此催生一种截然不同的研究工作流程？

Jesse Han：我想在这个问题上再补充一句。事实上，在数学史上，应该已经出现过不少并非基于形式化验证、也不依赖计算机的例子：某些更好的数学技术或方法被发明出来之后，使数学家得以摆脱以往的一些繁琐劳动，从而能够把精力投入到全新的问题和思考方式中。

我也很好奇，在解析数论的发展过程中，是否存在过这样的重要例子？比如，是否有某些关键方法的出现，真正改变了人们理解和研究这一领域的方式？

如果是这样的话，那么我们是否也可以把如今的形式化工具（如 Lean）以及自动形式化技术，视为历史上这一类技术演进的又一个实例，一次新的数学技术革命？

陶哲轩：我认为数论其实是最早采用实验性方法的数学分支之一。例如，数论中的一个核心问题，关于素数分布的规律，最早就是由高斯提出的猜想。

高斯当年通过一种极其艰苦的方式来获得直觉：他手工计算了前几十万、甚至上百万个素数，并从这些数据中观察到了某些模式，由此提出了后来影响深远的素数分布猜想。

从今天的角度看，这几乎就是一种早期的计算实验数学：通过大量具体数据的积累，来引导理论判断和猜想的形成。这在当时是非常开创性的做法，也深刻影响了数论此后的发展方向。

Jared Duker Lichtman：而且当时所依赖的，其实只是规模很小的数据。

陶哲轩：是的。高斯展现出了一种非凡的能力：他能够从规模非常小的数据集中，概括出极其深刻、普遍的规律，这正是高斯天才的体现，也正因为如此，后来很多工具都会以他的名字命名。

而随着计算技术的发展，我们才真正能够系统性地展开这种探索。后来也陆续出现了不少类似的例子：一些重要的猜想最初正是通过数值实验和计算探索被发现的；而在更近的时代，还有一些结果是借助大规模枚举，甚至结合机器学习方法，才逐渐显现出其结构和规律的。

这些进展都说明了一点：新的技术手段不断扩展着数学家可探索的空间，也在持续改变人们理解和研究数论的方式。

Jared Duker Lichtman：我想，甚至连图灵当年也在做类似的事情，亲自去计算函数的零点。

陶哲轩：像某些算术函数的研究，其实早期就大量依赖数值计算。比如黎曼猜想，在很长一段时间里，正是通过大量数值实验获得了强有力的支持。

因此，历史上早就存在这样的先例：计算机的引入，催生了一种新的数学研究方式，不再只是依赖纯粹的抽象思考，而是结合数据和实验来推动理论的发展。

当然，我们现在讨论的这种形式化工作，并不完全等同于数据驱动的数学，但它无疑是一种计算机辅助的研究模式。

Jared Duker Lichtman：那么，撇开机器学习领域里那一小部分人，或者少数主动尝试新工具的研究者不谈，对于一位普通的数学家来说，无论是在数论还是其他领域，在日常研究工作中，有多大比例其实是被这种繁琐、机械性的苦工所拖慢、所构成瓶颈的？

陶哲轩：这个问题其实很难给出一个精确的百分比，但我觉得关键并不在于直接统计时间比例，而在于一种间接影响。

正是因为这些繁琐劳动的存在，我们往往会有意识地改变做数学的方式，尽量减少自己要面对的苦工。比如，当我们意识到某一步组合推导开始变得非常凌乱、计算量巨大时，往往会选择刻意绕开，改用另一条思路继续推进。

因此，如果你只看最终论文里呈现出来的内容，会觉得我们似乎做的都是高判断力的工作，真正的苦工并不多。但那是因为我们在研究过程中，已经下意识地避开了道路上的一个个坑，用一个比喻来说，我们是在不断绕开崎岖路段，而不是去填平它们。

而一旦这些工具真正到位，情况可能会发生根本变化。那时，我们会改变做事方式：如果前方出现一个巨大而繁重的计算任务，我们不再选择绕路，而是直接碾过去，动用所有可用的技术手段，借助计算、形式化工具，甚至直接交给计算机，说清楚从这里到那里该怎么走，然后继续前进。

这样一来，我们就可以穿越那些现在几乎是下意识回避的障碍。所以，从表面上看，当前数学研究中苦工的比例似乎并不高；但如果把那些被我们主动规避掉的工作也算进去，那这个比例其实远比看上去要大得多。

Jesse Han：之前你提到过，一个非常重要的瓶颈在于：寻找合适的合作者本身就很困难，更不用说还要在工作方式、思路层面与他们建立足够的默契。

我想具体问的是：在这种情况下，你觉得在研究过程中，有多大比例的时间，其实是被人与人之间沟通、对齐思路、传递和同步这些界限结果所消耗的？也就是说，为了在人类专家之间完成某种分布式计算，我们究竟付出了多大的沟通成本？

以及，如果你所设想的这一愿景真的实现了形式化、自动化工具能够承担起这些传递与整合工作，你认为这一领域的数学研究整体上有可能被加速多少倍？

陶哲轩：我觉得确实如此。首先，这是一个信任问题。在这类计算密集的研究中，只要某一步出了错，整个推导就可能全部失效。因此，你必须清楚哪些作者是可靠的、哪些结果是可以放心使用的，而这些信息往往是隐性的，并不会明确写在论文里。

现实中，我们不会公开列出哪些工作存在严重问题，于是你只能依赖对学术共同体的熟悉程度：你得知道这个圈子，知道该去问谁。很多时候，如果某个结果还没有正式发表，但你认识相关领域的专家，就可以直接去问他：这个地方是不是只需要稍微改一下就行？对方可能就会给你一个可靠的判断。

这就形成了一个明显的瓶颈：你必须身处这个关系网络之中，认识足够多对的人，才能高效地在这个领域工作。

而一旦我们能够通过形式化工具（比如 Lean）提供这种可验证的信任保证，情况就会发生根本改变。那时，你可以放心使用来自陌生研究者的结果，即便你从未见过他们，因为所有证明都已经由系统严格验证过。

正是在这一点上，我认为形式化将会极大地解锁生产力，消除大量由于信任与沟通成本造成的阻塞，从而释放出此前被压抑的大量研究潜力。

Jared Duker Lichtman：是的，我明白你的意思。你刚才提到信任这个概念，其实在数学研究中，信任往往是通过长期积累的学术记录建立起来的。一个研究者在某个领域持续工作、不断产出成果，随着时间推移，其他人自然会越来越信任他的结论。

而真正让我开始对形式化和数学基础问题产生强烈兴趣的一个重要故事，正是关于一位数学家的经历。他曾经建立起极高的学术声誉，证明过许多非常了不起的结果，因此在学界拥有极强的可信度。

但在 20 世纪 90 年代末，他写过一篇论文，后来大约在十年之后，他才意识到其中存在一个关键性的错误。回过头来看，他自己也反思到：当时很多人之所以接受那篇结论，很大程度上是因为大家在相信他这个人，而不是因为证明本身被彻底、逐行地验证过。

而这正揭示了一个核心问题：个人声誉和过往记录，并不等同于真理的保证。这类经历也正是形式化证明与基础堡具如此重要的原因之一，它们提供的不是基于人的信任，而是基于可验证结构的信任。

陶哲轩：当然，这种做法在深度上是有极限的。我们能够推动数学前进的程度，终究会受到限制。当前在分析学中，这个问题相对没那么严重，是因为这里逐渐形成了一张不断加密的信任之网，而且我们的工作方式往往更接近从第一性原理出发，比其他一些领域更少依赖远距离的结果。

但即便如此，这种基于信任的结构依然是数学发展的一个限制因素。从长远来看，这是一个无法回避的问题，也是形式化和基础堡具之所以重要的又一个原因。

Jared Duker Lichtman：我想再追问一个相关的问题。随着我们开始系统性地回溯并形式化一些经典论文，以及从 20 世纪 60 年代以来的大量文献，你会如何看待这样一个问题：

第一，在现有的数学文献中，可能还存在多少尚未被发现的错误？

第二，这些错误中，有多少只是可以通过小修小补解决的技术性问题？换句话说，整个数学体系作为一个整体，对这类错误究竟有多强的鲁棒性？

也就是说，即便我们真的通过形式化手段暴露出大量隐藏的问题，它们是否大多不会动摇理论的核心结构，而只是需要局部修正？还是说，其中也可能存在少量但影响深远的根本性漏洞？

陶哲轩：说实话，我也很想知道实际的错误率到底是多少。也许结果会让我们惊喜，也可能会让我们不太愉快。等六个月之后再来问我吧。

Jesse Han：今天这次交流真的非常愉快，真希望能再多聊一会儿。那就希望六个月之后，我们还能再进行一次这样的对话。