陶哲轩12年前的预言，现在AI帮他兑现了

< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400"> 陶哲轩12年前的预言，现在AI帮他兑现了 闻乐 2026-06-20 19:56:57 来源： 量子位 全球最聪明的人之一，成了AI最狂热的布道者 闻乐 发自 凹非寺 量子位 | 公众号 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纳入自己的研究流程，也不断建议年轻学者要掌握与