量子位

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

8.5内容质量

TL;DR · AI 摘要

陶哲轩12年前预言AI将改变数学研究，如今通过Lean和AI协作实现形式化证明，推动数学研究进入新阶段。

核心要点

  • 陶哲轩预言AI将取代LaTeX，如今形式化语言与Lean系统已实现自动验证。
  • Equational Theories项目48小时内解决2200万个数学关系中的大部分问题。
  • Lean系统与AI协作，使数学证明形式化效率大幅提升。

结构提纲

按章节快速跳转。

  1. §引言

    陶哲轩12年前预言AI将改变数学研究，如今预言正在逐步实现。

  2. ·陶哲轩的预言与数学研究的未来

    陶哲轩预言计算机将自动验证数学证明，并用形式化语言取代LaTeX。

  3. ·协作数学的尝试与挑战

    陶哲轩参与Polymath项目，发现协作数学的验证难题。

  4. ·Lean系统与形式化证明

    Lean系统帮助陶哲轩实现形式化证明，推动数学研究进入新阶段。

  5. ·Equational Theories项目与AI协作

    陶哲轩发起Equational Theories项目，AI与Lean系统协同解决数学问题。

思维导图

用一张图看清主题之间的关系。

查看大纲文本（无障碍 / 无 JS 友好）
  • 陶哲轩的预言与AI协作数学
    • 预言内容
      • 形式化语言取代LaTeX
      • 计算机自动验证数学证明
      • 大规模协作数学成为常态
    • 实现路径
      • Lean系统
      • AI协作
      • Equational Theories项目

金句 / Highlights

值得收藏与分享的关键句。

#数学#AI#Lean#协作#形式化证明
打开原文

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

扫码关注量子位

<div class="top_search"> <form role="search" method="get" class="search-form" action="https://www.qbitai.com/" id="search"> <label> <input type="search" class="search-field" placeholder="搜索…" value="" name="s"> </label> <button type="submit" class="search-submit"></button> </form> </div>

< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">

articlead begin

articlead end

陶哲轩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纳入自己的研究流程，也不断建议年轻学者要掌握与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，它居然直接把我拉进去玩儿了一把？！ 2026-06-19
  • 微信支付发布AI专属卡 WorkBuddy率先接入 2026-06-17
  • Claude Fable 5首日实测，杀疯了… 2026-06-10
  • Anthropic老大的唯一 -1，就是AI股神的未婚妻 2026-06-12

左侧分享

扫码分享至朋友圈

相关阅读 start

相关阅读

#### 陶哲轩转发！DeepMind开源「AI数学证明标准习题集」

所有人都能加入共创

明敏

2025-05-31

#### 啥？陶哲轩18个月没搞定的数学挑战，被这个“AI高斯”三周完成了

创始人是ICML'25时间检验奖作者

十三

2025-09-14

ICML 2025

素数定理

#### 陶哲轩在线安利Claude Code：审稿意见全给它，15分钟欧了

还反向挑出审稿人的毛病

鹭羽

2026-05-06

数学

#### 黎曼猜想获显著突破，陶哲轩：方法巧妙且意想不到！36岁菲尔兹奖得主新成果

破解80年未有实质性改进的数学问题

鱼羊

2024-06-05

詹姆斯·梅纳德

黎曼猜想

#### 陶哲轩用GPT5-Pro跨界挑战！3年无解的难题，11分钟出完整证明

总结“AI在小尺度有用、中尺度无益、大尺度又有帮助”

2025-10-11

#### 陶哲轩推荐：2高中生发现勾股定理新证明，论文已发《美国数学月刊》

5-10个新证明

2024-10-30

勾股定理

相关阅读 end

热门文章 start

热门文章

#### HuggingFace CEO力荐，Bengio团队也押注：这个1500美元训出的HRM模型，凭什么火了？

2026-06-13

#### 智源大会 | 天工AI重新定义世界模型，公布Matrix-Game 3.5 最新技术突破

2026-06-15

#### 三连发！阿里发布首个具身大模型Qwen-Robot系列

2026-06-16

#### 困住医疗AI的死循环，终于有国产玩家跑通了

2026-06-17

#### 为什么最有价值的AI讨论总发生在知乎？

<form role="search" method="get" class="search-form" action="https://www.qbitai.com/"> <label> <span class="screen-reader-text">搜索：</span> <input type="search" class="search-field" placeholder="搜索…" value="" name="s" /> </label> <button type="submit" class="search-submit"><span class="screen-reader-text">搜索</span></button> </form>

热门文章 end

底部版权

  • 关于量子位
  • 加入我们
  • 寻求报道
  • 商务合作

<a href="/?page_id=183"target="_blank"><i class="weixin_icon"></i></a>

追踪人工智能新趋势，报道科技行业新突破

<p>量子位 QbitAI 版权所有©北京极客伙伴科技有限公司 京ICP备17005886号-1</p>

量子位 QbitAI 版权所有©北京极客伙伴科技有限公司 京ICP备17005886号-1