事实证明，菲尔兹奖得主有时候也兼职预言家。

12 年前，陶哲轩在首届数学突破奖的台上抛出的一句预言，被视作天方夜谭：

将来有一天，我们或许不再用 LaTeX 撰写论文，而是使用计算机能理解的的形式化语言。

那一年，Transformer 还没诞生，ChatGPT 更是连影子都没有。

没想到，回旋镖正中靶心。过去这一年，AI 在数学领域突然开始疯狂提速。

从 OpenAI 解决开放问题，到 DeepMind 批量攻克数学猜想，越来越多数学证明被写进形式化系统，交给计算机自动验证。

回望来路，最早看清风向、亲自下场实践的人，就是陶哲轩。

十年间，他先后推进大规模协作数学、Lean 形式化证明、又发起 Equational Theories 项目，面对 2200 万个数学问题，依靠「AI+ 人类协作」，短短 48 小时就攻克大半。

项目在 AI 助力下效率拉满，很多时候连他本人都不用插手了。

实际上，陶哲轩这也是用实际行动证明，最好的预测未来，就是亲手把它创造出来。

神童，但更迷恋协作

说起陶哲轩，很多人第一反应是那串传奇经历：

2 岁时教比自己大的孩子数数，7 岁开始接触微积分，10 岁成为国际数学奥林匹克史上最年轻的铜牌得主，24 岁成为 UCLA 历史上最年轻的终身教授之一，31 岁拿下菲尔兹奖。

72 岁的保罗・埃尔德什与 10 岁的陶哲轩 图源：Quantamagazine

在大众印象里，这样的人往往属于"天才独行侠"。

但陶哲轩本人恰恰相反。

相比于孤军奋战，他一直对另一件事更感兴趣：

数学家能不能像开源软件开发者一样协作？

一个人知道 A，一个人知道 B，如果把两个人的知识拼起来，会不会出现单个人想不到的新东西？

这种想法后来深刻影响了他的整个职业生涯。

2009 年，他参与了Polymath 项目，一个把数学协作搬上公开论坛的实验。

在这个项目里，任何人都可以登录，认领子问题，提交思路，群策群力。

原本需要少数专家花费数月甚至数年完成的问题，在公开协作模式下被快速推进。

这次实验最终成功解决了一个组合数学问题，证明了大规模协作在数学上不是空想。

Polymath 成功了，但陶哲轩很快发现一个更大的问题：

所有的错误核查，都压在核心负责人身上。

参与者越多，审核压力越大；协作规模越大，组织成本越高。

没有自动验证工具，人工纠错的速度永远跟不上协作的规模。协作数学的上限，被压住了。

要突破这道天花板，必须找到别的路。

2014 年，他在首届突破奖的台上，描述了自己眼中的未来数学，也就是三个当时听起来不太靠谱的预言：

数百人规模的大规模数学协作会成为常态；

计算机将能自动验证数学证明；

LaTeX 会被机器能读懂的形式化语言所取代。

今天看，这三个判断几乎对应了 AI 数学发展的全部主线。

但放在当时，它们听起来过于超前。

虽然 Polymath 证明了协作数学行得通，但如果不能把"验证"这件事自动化，数学研究很难真正实现规模化协作。

而他等待的答案，最终出现在一种名叫Lean的工具身上。

预言说了十年，他决定亲自试试

转机出现在 2023 年。

那一年，陶哲轩在一次交流中认识了数学家 Kevin Buzzard，这位也是 Lean 的早期推广者。

Lean 是一套交互式定理证明系统，用形式化语言描述数学证明，让计算机逐行验证每一步的逻辑。

这套理念恰好击中了陶哲轩多年来思考的问题，于是，在 Buzzard 的鼓励下，48 岁的陶哲轩决定亲自下场实践。

2023 年 10 月 9 日，他在社交媒体上发了条状态：

我决定终于开始学习 Lean4 交互式证明系统了（必要时使用 AI 协助）。

这位菲尔兹奖得主原本觉得，这不会太难，于是挑了一道关于麦克劳林不等式的问题作为练手项目，打算以此为素材，尝试用 Lean 完成证明形式化。

他先按传统写法完成 10 页手写风格证明，再着手将其转译为 Lean 代码。按照他的估计，大概一周左右就能搞定。

然后，他碰壁了。

上手后他发现，形式化证明和写数学论文是两种完全不同的思维模式。

在传统论文里，一句"三个大于 1 的数相加大于等于 3 "几乎没人会多看一眼，但 Lean 不行：

你必须明确告诉系统你引用的结论来自哪里？对应哪一个引理？

很多看似显然的步骤，都需要补上大量形式化细节，原本几行纸面推导，很容易变成数百行代码。

一个月后，陶哲轩终于完成自己的第一个正式化证明。

虽然代码并不优雅，但从那一天开始，他真正成为了形式化数学社区的一员。

PFR 项目：预言第一次落地

在他学习 Lean 不久后，就出现了一个新的机会。

2023 年 11 月 9 日，陶哲轩和合作者 Ben Green、Tim Gowers 等人完成了一篇关于 PFR 猜想的论文。

这是一个关于集合加法结构的数论命题，此前悬而未决多年。

论文写完了，但他没停。接着，他在 Lean 社区发了一篇帖子：

大家好，我准备启动一个项目，把 PFR 猜想的最新证明在 Lean4 里正式化……欢迎任何人参与。

这次和 Polymath 最大的不同在于，Lean 负责审查。

这一次，他把论文拆成了一块块可以独立认领的子任务，开放给全球社区。

每个人完成自己的一块，系统自动核验，通过了才能合并进主线。

结果全程仅三周，所有形式化工作全部完成。

甚至，陶哲轩发布了一个额外的小任务，不到 1 小时就有社区成员完成并提交。

这也是他第一次看到自己十多年前设想的协作数学模式，真的能运转起来。

2200 万种数学关系，48 小时确定大半

尝到甜头之后，他把赌注押得更大了。

2024 年 9 月 25 日，陶哲轩发起了Equational Theories 项目，目标是系统性地确定约 2200 万个代数等式之间的逻辑蕴含关系。

简单说，就是搞清楚哪些方程式能从哪些方程式推导出来。

这次陶哲轩用上了全新组合：AI 帮忙写证明，Lean 负责检查对错，全球志愿者社区分头攻克具体难题，三方协同推进工作。

自动化证明助手工作流程 图源：Quantamagazine

这次结果出得更快！48 小时内，大规模筛选基本完成，大量问题已经解决在望。

前 9 天，整体进度已推进到 99.866%，第 57 天，主项目宣告基本完工，只剩 162 个蕴含关系等待收尾。

甚至，这个项目还在过程中催生了一个全新的数学概念magma cohomology（原群上同调）。

这个概念是为无公理约束的原群量身打造的上同调理论，核心是定义了依赖等式的上同调群 H ¹、H ²，用于分类原群扩张、构造反例、区分不同原群，是经典群上同调的推广，用来研究最一般的代数结构。

除此之外，Equational Theories 项目展现出的自主运转能力，也让陶哲轩欣喜。

依托 AI 辅助与自动化核验，即便他不全程跟进，各项工作也能稳步推进。

过去两年里，陶哲轩已经越来越频繁地把 AI 纳入自己的研究流程，也不断建议年轻学者要掌握与 AI 协作的能力。

从陶哲轩身上可以看到的是，最好的预言家，其实是先行者——

不止于预判未来，亲身实践，一步步把曾经的设想变为现实。

如今，这位先行者也已经成为 AI 数学最坚定的布道者。

参考链接：

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

[ 2 ] https://terrytao.wordpress.com/2023/11/

[ 3 ] https://gowers.wordpress.com/2009/03/10/

—  欢迎 AI 产品从业者共建  —

� �「AI 产品知识库」是量子位智库基于长期产品库追踪和用户行为数据推出的飞书知识库，旨在成为 AI 行业从业者、投资者、研究者的核心信息枢纽与决策支持平台。

一键关注 � � 点亮星标

科技前沿进展每日见