---
layout: post.njk
source: https://baoyu.io/blog/2026-03-04/terence-tao-mathematics-in-the-age-of-ai
speaker: baoyu.io
title: 陶哲轩最新演讲：AI 不是来抢数学家蛋糕的，是来把蛋糕做大的 | 宝玉的分享
date: '2026-03-04'
summary: 陶哲轩的最新演讲指出，AI 并非数学家的替代者，而是拓展数学研究疆域的强大工具。演讲强调了形式验证在促进大规模数学协作中的关键作用，以及 LLM 在生成和检验数学问题上的潜力与局限。AI 的核心价值在于处理海量中等难度问题，扩大研究规模，而非直接攻克最尖端难题。通过 GitHub 和 Zulip 等平台，AI 正在重塑数学研究的工作流，使其更具可扩展性和协作性。
area: tech-engineering
category: ai-application
tags:
  - ai-in-math
  - formal-verification
  - collaboration
  - large-language-models
people:
  - Terence Tao
companies_orgs:
  - SAIR Foundation
  - UCLA
  - IPAM
  - Google DeepMind
products_models:
  - Lean
  - AlphaEvolve
  - Gemini
media_books: []
draft: true
status: evergreen
---

宝玉的分享

Menu

See all posts

Published on 2026-03-04

# 陶哲轩最新演讲：AI 不是来抢数学家蛋糕的，是来把蛋糕做大的

作者：

宝玉

陶哲轩办公室有 6 块黑板，他说绝不放弃。但他刚带 50 个人用 AI 和代码解决了 2200 万道数学题。

这位 Fields 奖得主在 2026 年 2 月的 SAIR 基金会“AI for Science: Kickoff 2026”活动上，用 17 分钟讲了一件事：数学这个几百年没变过工作方式的领域，正在被新技术撬动。 而撬动它的关键，不是 AI 本身，而是一个大多数人没听说过的东西。

原始视频链接：https://www.youtube.com/watch?v=mS9Lr43cIB4

要点速览：

数学可能是最保守的学科：200 年前的教材今天还能用，数学家是最后还在用粉笔黑板的学术群体

数学家不爱协作有结构性原因：准入门槛高、容错率为零、工作流无法扩展到互联网规模

形式验证是大规模数学协作的“秘密武器”，它打破了信任壁垒，让匿名贡献成为可能

陶哲轩主导的等式理论项目在三个月内解决了 2200 万个代数问题，此前同类项目只处理过约 20 个

LLM 能解奥赛题但连简单算术都会出错，必须配合验证器才能在数学中发挥作用

AI 对数学最大的价值不是替代数学家攻克最难的问题，而是处理人类没精力覆盖的海量中等难度问题

> 注： SAIR（Foundation for Science and AI Research）是陶哲轩联合创办的非营利基金会，致力于用 AI 加速科学发现。本次活动由 SAIR 与 UCLA 的 IPAM 联合举办。

## 200 年前的课本，今天还能用

陶哲轩在演讲开头展示了一本 1826 年 Cauchy 写的数学教科书。

> 除了是用法语写的、不是用现代排版工具排的，跟我们今天给研究生用的几乎一模一样。
> （“Other than it's in French rather than English and it's not typeset using a modern computer language... it's completely usable today.”）

这种 200 年的连续性是数学的力量。勾股定理是两千多年前的成果，陶哲轩说他自己的研究中经常使用。但代价是：数学家极度保守，几乎是最不愿拥抱变化的学术群体。

他举了一个有趣的细节：数学家恐怕是唯一还守着黑板和粉笔的学术学科了。其他领域早就换成了 PPT 和白板。摄影师 Jessica Wynne 甚至专门拍了一本数学家黑板的摄影集《Do Not Erase》（别擦掉），出版后成了一本艺术画册。

> 注：《Do Not Erase》由 Princeton University Press 于 2021 年出版，收录了 100 多位数学家的黑板照片，陶哲轩的黑板也被拍进去了。

而陶哲轩自己呢？

> 我办公室有 6 块黑板。我爱它们。我不会放弃的。
> （“I have six blackboards in my own office. I love them. I will not give them up.”）

## 为什么数学不能像其他科学那样搞大规模协作

陶哲轩展示了一张各学科论文平均作者数的变化图。其他科学领域的协作人数在爆炸式增长，数学呢？从 1.5 人缓慢爬到了 2.5 人。

他自嘲说，不是因为数学家反社会，或者说“不只是因为反社会”。真正的原因有三个：

第一，门槛太高。 你通常得有数学博士学位才能理解自己在做什么问题。

第二，正确性要求极端。 如果你众包一个证明，100 份贡献里有 1 份是错的，整个证明就废了。

> 如果你尝试众包一个证明，100 个贡献中有一个是错误的，就毁掉了整个证明。
> （“If you try to crowdsource a proof and there's 100 contributions and one of them is incorrect, you destroy the whole proof.”）

第三，工作流没法扩展。 数学家的核心工作方式是两三个人站在黑板前讨论，这没法 scale 到 100 人在线协作。

但其他科学已经在这样做了，而且蓬勃发展。

数学是不是错过了什么？

## 从一次一题到一次百万题

陶哲轩说，变化正在发生。他用了一个精辟的框架来描述：过去的数学研究是“案例研究”模式，一次挑一个问题，花几个月产出一篇论文，再去做下一个。现在开始出现“大规模调查”模式，同时处理数百甚至数千个问题。也许不能全部解决，但可以报告这些问题群体的有趣统计规律。

参与者也在拓宽。其他学科的“公民科学”已经很成熟了，数学才刚开始出现“公民数学”。

> 注： 公民科学（citizen science）指非专业科学家参与科研项目，比如天文爱好者帮助分类星系图像。数学领域此前很少有这种模式。

至于 AI？陶哲轩的措辞很有意思：

> 我们发现了很多使用机器学习和 AI 的错误方式，但才刚开始从这些工具中获得一些有用的价值。
> （“We've discovered lots of incorrect ways to use machine learning and AI, but we're just beginning to get some useful mileage out of these tools.”）

而让这一切成为可能的，有一个”秘密武器”。

## 秘密武器：形式验证

这个秘密武器不是 AI，而是形式验证（formal verification）。

简单说，形式验证是一种特殊的计算机语言，能接收一段数学论证，自动判断它对不对。陶哲轩说，这一个能力就“过滤掉了大量垃圾”，移除了此前阻碍新工作流的最大障碍。

为什么这么重要？因为它直接解决了前面提到的“100 份贡献里 1 份错误就毁掉整个证明”的问题。有了自动检查，你不再需要信任每个贡献者，只需要信任验证系统。

> 注： 目前数学形式化领域最活跃的工具是 Lean，由微软研究院开发的证明助手语言。它不仅能验证证明对不对，还能像 IDE 一样在写证明过程中实时提示哪一步出了问题。

## 2200 万道代数题，50 个人，三个月

陶哲轩花了最多篇幅讲这个案例：Equational Theories Project（等式理论项目）。

他在 UCLA 发起了这个项目，共 50 位协作者参与。但这些人大多数他从未见过面，是通过项目才认识的；大多数也不是专业数学家，而是计算机科学家、研究生、本科生，他说甚至可能有高中生。

项目的任务是：程序化生成了 2200 万道代数蕴含关系问题。比如，如果一个运算满足交换律（a*b = b*a），能推出它也满足结合律（(a*b)*c = a*(b*c)）吗？答案是不能。但这样的问题有 2200 万个。

> 注： 准确地说，是 4694 个 magma（只有一个二元运算的代数结构）等式定律之间的两两蕴含关系，共 22,028,942 对。项目于 2024 年 9 月 25 日在 GitHub 上启动，最终论文于 2025 年 12 月上传 arXiv。

单独来看，每道题可能一个代数方向的研究生花一小时就能解。但 2200 万道？

> 我可没有 2200 万个研究生。
> （“I don't have 22 million grad students.”）

你可以说“那就众包吧”，但谁来批改 2200 万道题？以前同类型的研究最多处理过 20 个问题。

他们三个月就做完了。每一道都有证明或反证。

怎么做到的？所有证明存在 GitHub 上，必须用 Lean 语言形式化，这样就能自动验证正确性。协作讨论在 Zulip（一个开源的类 Slack 平台）上进行。有人写出人类可读的证明，有人把它翻译成 Lean 代码；有人写程序批量攻克问题，一次处理 10 万道；有人则把计算机证明转化回人类证明。大量来回迭代，虽然是即兴摸索出来的，但效果极好。

## 为什么这个项目能成功

陶哲轩总结了几个关键因素。

第一是模块化。 2200 万个问题天然地拆分成子任务，每个人可以认领一批来做。有人专写人类证明，有人专做 Lean 翻译，不需要理解项目全貌就能贡献。他类比说，”就像现代软件开发项目”。

第二是有一个明确的指标。 在项目第 16 天，2200 万个蕴含关系中只剩 888 个未解决。这个数字就是所有人的目标，把它往下推。有些想法一次能消掉一大批，有些没那么成功。但不需要全局协调，每个人都在自发地把数字往下推。陶哲轩说，参与者的自发行动“看着真的很有趣”。

第三，也是最关键的：形式验证打破了信任壁垒。

以前数学协作的模式是：要么逐行检查别人的工作，要么靠声誉信任对方。但这个项目收到了大量来自陌生人的贡献，有些人从未在数学界露过面。这没关系，所有提交都必须通过 Lean 的自动验证。匿名贡献？可以。不受信任的贡献？也可以。

而且形式验证让讨论变得极其精确。比如有人提交了一个九步证明，前八步都通过了，第九步 Lean 报错。这时候你可以就那一个微小的步骤跟作者讨论。以前没有共同的精确语言，很难定位到底卡在哪一步；现在可以在“原子级别”上进行技术对话。

整个项目中，虽然也用了自动化定理证明器之类的 AI 工具，但陶哲轩坦言：

> 实际上起作用的是更平凡的技术，就是 GitHub 和 Zulip 这些基本的协作平台，它们简直太有用了。
> （“Actually it was the more mundane technologies, things just like GitHub and this discussion group at Zulip. Basic collaboration platforms were just incredibly useful and essential.”）

> 注： Zulip 是一个开源的群组讨论平台，类似 Slack 但有独特的”话题线程”功能，特别适合技术讨论。Lean 数学社区的主要交流平台就是 Zulip。

## LLM 能解奥赛题，但连乘法都会算错

演讲进入下半段，陶哲轩转向 AI 和大语言模型。

LLM 越来越强大了，能解数学奥赛题，有时能回答很深的数学问题。但它们会犯错误，而且经常是非常基础的错误。陶哲轩展示了一个例子：某 LLM 被问 7×4+8×8 等于多少，算错了。被指出后道歉，然后给出了正确答案。

每个数学家都试过用 LLM。结论呢？

> 每个数学家最终都发现，不可靠性是一个太大的问题。
> （“Every mathematician has tried using these and has eventually found that the unreliability is too great of an issue.”）

但如果把不可靠的 LLM 输出和一个验证器结合起来呢？让 LLM 生成数学输出，验证器检查是否正确；正确就保留，不正确就把错误信息反馈给 LLM 让它纠正。这个“生成→检验→反馈→纠正”的循环，有时候能跑通。

陶哲轩正在跟 Google DeepMind 合作他们最新的工具 AlphaEvolve。这个工具不只是 LLM，底层还有遗传算法。

> 注： AlphaEvolve 是 Google DeepMind 开发的”进化式编程智能体”，结合 LLM（Gemini）的代码生成能力和进化算法，通过不断提出、测试、优化代码方案来解决数学和科学问题。2025 年 5 月公开宣布，同年 11 月陶哲轩等人在 arXiv 发表了使用 AlphaEvolve 攻克 67 个数学问题的论文。

他举了一个例子：如果你有 11 个正六边形，能装进去的最小正六边形多大？以前有人类找到的最优记录，AlphaEvolve 通过让 LLM 不断尝试、获取反馈、进化代码，打破了这些记录。

但这些只是测试案例。堆叠问题本质上是有限维优化，只是数学家关心的问题的一个很小的子类。陶哲轩透露，他们在无穷维优化问题上也有了新进展，但”很遗憾，暂时还不能说更多。请关注，几周后我们会发论文。”

## 不是来抢蛋糕的，是来把蛋糕做大的

演讲收尾，陶哲轩总结了 AI 对数学的影响。

已经在发挥作用的场景：

写代码比以前容易太多了

文献综述已经是很好用的应用

有零星案例显示 AI 能从数据集中发现新的数学猜想

AI 是很好的“万能翻译器”，帮助数学家跟公众和其他学科沟通，因为各自的术语体系不同

但要获得更高级的应用，必须依赖严格的验证。AI 单独辅助个体数学家有一定帮助，但和更广泛的协作体系结合时效果最大，它能填补协作中缺失的环节。

> 我们只能在信任 AI 输出的范围内使用它，或者至少能检查它。超出这个范围就太冒险了。
> （“We can only use the AI as far as you can trust its outputs, or at least check them. Any further and it's just too risky.”）

然后他提出了一个和常见想象不同的观点。大家最容易想到的 AI 用途，是用 AI 替代数学家做他们最擅长的事，用创造性的新技术攻克难题。但有一个“正交”的用途，至少在中期内会更有生产力。

数学中存在一条巨大的“中等难度问题长尾”，就像那 2200 万道代数题。人类没有人力一个个去做，但可以让 AI 先跑一遍，把简单的都解决掉，然后把真正难的上报给人类专家。

> AI 不应该跟人类已经在做的工作竞争，而应该把蛋糕做大，创造出更多任务，让更多目标在经济上变得可行。
> （“AI should be used to not compete with the pie of work that humans already do, but to enlarge the pie and create more tasks — make more objectives economically feasible.”）

他最后补充：这些应用都非常依赖具体场景，不是即插即用的。得知道什么时候该用、怎么用。

完整演讲视频：https://www.youtube.com/watch?v=mS9Lr43cIB4

See all posts

Built by 宝玉.  RSS . 本站原创内容，独家授权赛博禅心公众号发布。

Toggle theme