闻乐 发自 凹非寺

量子位 | 公众号 QbitAI

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

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数学最坚定的布道者。