Full text · 原文
3,070 字
闻乐 发自 凹非寺<br>
量子位 | 公众号 QbitAI<br>
事实证明，菲尔兹奖得主有时候也兼职预言家。<br>
12年前，陶哲轩在首届数学突破奖的台上抛出的一句预言，被视作天方夜谭：<br>
将来有一天，我们或许不再用LaTeX撰写论文，而是使用计算机能理解的的形式化语言。<br>
那一年，Transformer还没诞生，ChatGPT更是连影子都没有。<br>
没想到，回旋镖正中靶心。过去这一年，AI在数学领域突然开始疯狂提速。<br>
从OpenAI解决开放问题，到DeepMind批量攻克数学猜想，越来越多数学证明被写进形式化系统，交给计算机自动验证。<br>
回望来路，最早看清风向、亲自下场实践的人，就是陶哲轩。<br>
十年间，他先后推进大规模协作数学、Lean形式化证明、又发起Equational Theories项目，面对2200万个数学问题，依靠「AI+人类协作」，短短48小时就攻克大半。<br>
项目在AI助力下效率拉满，很多时候连他本人都不用插手了。<br>
实际上，陶哲轩这也是用实际行动证明，最好的预测未来，就是亲手把它创造出来。<br>
神童，但更迷恋协作<br>
说起陶哲轩，很多人第一反应是那串传奇经历：<br>
2岁时教比自己大的孩子数数，7岁开始接触微积分，10岁成为国际数学奥林匹克史上最年轻的铜牌得主，24岁成为UCLA历史上最年轻的终身教授之一，31岁拿下菲尔兹奖。<br>
△72岁的保罗・埃尔德什与10岁的陶哲轩 图源：Quantamagazine<br>
在大众印象里，这样的人往往属于“天才独行侠”。<br>
但陶哲轩本人恰恰相反。<br>
相比于孤军奋战，他一直对另一件事更感兴趣：<br>
数学家能不能像开源软件开发者一样协作？<br>
一个人知道A，一个人知道B，如果把两个人的知识拼起来，会不会出现单个人想不到的新东西？<br>
这种想法后来深刻影响了他的整个职业生涯。<br>
2009年，他参与了Polymath项目，一个把数学协作搬上公开论坛的实验。<br>
在这个项目里，任何人都可以登录，认领子问题，提交思路，群策群力。<br>
原本需要少数专家花费数月甚至数年完成的问题，在公开协作模式下被快速推进。<br>
这次实验最终成功解决了一个组合数学问题，证明了大规模协作在数学上不是空想。<br>
Polymath成功了，但陶哲轩很快发现一个更大的问题：<br>
所有的错误核查，都压在核心负责人身上。<br>
参与者越多，审核压力越大；协作规模越大，组织成本越高。<br>
没有自动验证工具，人工纠错的速度永远跟不上协作的规模。协作数学的上限，被压住了。<br>
要突破这道天花板，必须找到别的路。<br>
2014年，他在首届突破奖的台上，描述了自己眼中的未来数学，也就是三个当时听起来不太靠谱的预言：<br>
数百人规模的大规模数学协作会成为常态；<br>
计算机将能自动验证数学证明；<br>
LaTeX会被机器能读懂的形式化语言所取代。<br>
今天看，这三个判断几乎对应了AI数学发展的全部主线。<br>
但放在当时，它们听起来过于超前。<br>
虽然Polymath证明了协作数学行得通，但如果不能把“验证”这件事自动化，数学研究很难真正实现规模化协作。<br>
而他等待的答案，最终出现在一种名叫Lean的工具身上。<br>
预言说了十年，他决定亲自试试<br>
转机出现在2023年。<br>
那一年，陶哲轩在一次交流中认识了数学家Kevin Buzzard，这位也是Lean的早期推广者。<br>
Lean是一套交互式定理证明系统，用形式化语言描述数学证明，让计算机逐行验证每一步的逻辑。<br>
这套理念恰好击中了陶哲轩多年来思考的问题，于是，在Buzzard的鼓励下，48岁的陶哲轩决定亲自下场实践。<br>
2023年10月9日，他在社交媒体上发了条状态：<br>
我决定终于开始学习Lean4交互式证明系统了（必要时使用AI协助）。<br>
这位菲尔兹奖得主原本觉得，这不会太难，于是挑了一道关于麦克劳林不等式的问题作为练手项目，打算以此为素材，尝试用Lean完成证明形式化。<br>
他先按传统写法完成 10页手写风格证明，再着手将其转译为Lean代码。按照他的估计，大概一周左右就能搞定。<br>
然后，他碰壁了。<br>
上手后他发现，形式化证明和写数学论文是两种完全不同的思维模式。<br>
在传统论文里，一句“三个大于1的数相加大于等于3”几乎没人会多看一眼，但Lean不行：<br>
你必须明确告诉系统你引用的结论来自哪里？对应哪一个引理？<br>
很多看似显然的步骤，都需要补上大量形式化细节，原本几行纸面推导，很容易变成数百行代码。<br>
一个月后，陶哲轩终于完成自己的第一个正式化证明。<br>
虽然代码并不优雅，但从那一天开始，他真正成为了形式化数学社区的一员。<br>
PFR项目：预言第一次落地<br>
在他学习Lean不久后，就出现了一个新的机会。<br>
2023年11月9日，陶哲轩和合作者Ben Green、Tim Gowers等人完成了一篇关于PFR猜想的论文。<br>
这是一个关于集合加法结构的数论命题，此前悬而未决多年。<br>
论文写完了，但他没停。接着，他在Lean社区发了一篇帖子：<br>
大家好，我准备启动一个项目，把PFR猜想的最新证明在Lean4里正式化……欢迎任何人参与。<br>
这次和Polymath最大的不同在于，Lean负责审查。<br>
这一次，他把论文拆成了一块块可以独立认领的子任务，开放给全球社区。<br>
每个人完成自己的一块，系统自动核验，通过了才能合并进主线。<br>
结果全程仅三周，所有形式化工作全部完成。<br>
甚至，陶哲轩发布了一个额外的小任务，不到1小时就有社区成员完成并提交。<br>
这也是他第一次看到自己十多年前设想的协作数学模式，真的能运转起来。<br>
2200万种数学关系，48小时确定大半<br>
尝到甜头之后，他把赌注押得更大了。<br>
2024年9月25日，陶哲轩发起了Equational Theories项目，目标是系统性地确定约2200万个代数等式之间的逻辑蕴含关系。<br>
简单说，就是搞清楚哪些方程式能从哪些方程式推导出来。<br>
这次陶哲轩用上了全新组合：AI帮忙写证明，Lean负责检查对错，全球志愿者社区分头攻克具体难题，三方协同推进工作。<br>
△自动化证明助手工作流程 图源：Quantamagazine<br>
这次结果出得更快！48小时内，大规模筛选基本完成，大量问题已经解决在望。<br>
前9天，整体进度已推进到99.866%，第57天，主项目宣告基本完工，只剩162个蕴含关系等待收尾。<br>
甚至，这个项目还在过程中催生了一个全新的数学概念magma cohomology（原群上同调）。<br>
这个概念是为无公理约束的原群量身打造的上同调理论，核心是定义了依赖等式的上同调群H¹、H²，用于分类原群扩张、构造反例、区分不同原群，是经典群上同调的推广，用来研究最一般的代数结构。<br>
除此之外，Equational Theories项目展现出的自主运转能力，也让陶哲轩欣喜。<br>
依托AI辅助与自动化核验，即便他不全程跟进，各项工作也能稳步推进。<br>
过去两年里，陶哲轩已经越来越频繁地把AI纳入自己的研究流程，也不断建议年轻学者要掌握与AI协作的能力。<br>
从陶哲轩身上可以看到的是，最好的预言家，其实是先行者——<br>
不止于预判未来，亲身实践，一步步把曾经的设想变为现实。<br>
如今，这位先行者也已经成为AI数学最坚定的布道者。<br>
参考链接：<br>
[1]https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/<br>
[2]https://terrytao.wordpress.com/2023/11/<br>
[3]https://gowers.wordpress.com/2009/03/10/