陶哲轩：AI 让证明多到读不完，数学进入 2.0 时代
本文是视频《陶哲轩：AI 让证明多到读不完，数学进入 2.0 时代》（作者：Terence Tao（SAIR / Science x AI Summit））的精读笔记，配套中配视频观看效果更佳；另附完整文稿。
菲尔兹奖得主陶哲轩在 Science x AI Summit（UCLA）的这场演讲里抛出一个判断：数学正在经历三千年来的第一次范式升级——从沿用至今的「数学 1.0」走向「数学 2.0」。他不惊叹 AI 多强，而是拆解了三件事：AI 为什么恰好强在数学、「数学要被解决」的恐慌为何是误读、以及真正的风险藏在哪里。对关心 AI 与智力工作未来的人，这是一线视角的全景。
图：视频精读笔记 · 陶哲轩：AI 让证明多到读不完
图：全片论证主线：三要素 → 证明过剩 → 目标错位 → 数学 2.0
全景：一条主线看懂
解纯数学题恰好集齐机器学习最爱的三要素——可客观验证、可完全数字化、有大规模高质量数据集，于是 AI 突然擅长解题，数学进入「证明过剩时代」；证明过剩反过来让「解题」这个传统中心目标失效，因为机器给得出答案却给不出理解；出路就是数学 2.0——扩大研究前沿、弱化解题的中心地位，并在理解题意、解题、提新问题每一环用 AI 加固人的理解，而不是替人思考。
为什么偏偏是数学：三要素全中
AI 已经在颠覆创意艺术、科学、编程，如今轮到人类公认最难的智力领域之一。陶哲轩先划清范围：不是全部数学，而是「解纯数学问题」这一特定类别——它恰好是数学家工作的一大块。
他的论证框架是纯数学题的三个特点：其一，客观可验证，无论人或 AI 声称证明了，纸笔或计算机即可检验，如同认真审稿；其二，可数字化，不需要临床试验、脏数据或物理接口，解题全程可在计算机内完成；其三，大规模高质量数据集，几千年积累的教科书与论文就是天然精编的好数据。他拿癌症研究作反面对比：病人数据乱、不完整、受隐私法限制，医院不愿汇成共享库；数学却坐拥海量公开文献。三条恰好就是让机器学习强大的三要素，齐备则效果惊人——我们由此进入「证明过剩时代」。他也预警，这场升级会「有点动荡，但最终令人兴奋」，需要大量过渡工作、文化变革与包括开源模型在内的新基础设施。
图：演讲现场 · 从「解题稀缺」到「证明过剩」的三要素论证
本节要点：不是「AI 学会了数学」，而是「数学恰好长成了 AI 最擅长处理的样子」——可验证、可数字化、数据丰富。
证明过剩之后：解题这个「代理指标」失效了
几千年来数学处于证明稀缺时代：解题极难所以珍贵，重大问题被攻克时全领域同行放下手头一切去研究、开研讨会。如今彻底反转——陶哲轩自曝，他感兴趣的十几个结果已被证出，却没时间读任何一篇，只盼有人替他读。
他提醒 AI「参差不齐」的本性：连「strawberry 里有几个 r」都会数错，既非超人也非废物。针对「数学被解决、数学家失业」的担忧，他的反驳是：数学无限，能提出无限多问题，但人只做前沿问题；前沿有限却在永远扩张，且自我强化——进步越多，前沿越大。
更深的问题是目标错位：解题从来只是代理指标，机器能给出答案，却不带来理解、交流、合作、带学生这些解题天然附带的好处——数学 1.0 里解题之所以健康，正在于这些外溢效应。至于社媒上「AI 解题神了」，他拆穿为选择偏差：OpenAI 高调发布 300 个解答，脚注却写着实际尝试 4000 题、成功率约 9%；91% 的失败无人传播。
图：演讲现场 · 把目标与数学的长期健康对齐
本节要点：证明从稀缺变过剩，解题作为「代理指标」随之失效；AI 给答案不给理解，而理解才是数学 1.0 真正的产出。
两场实验：2200 万道题与 25000 枚「彩蛋」
陶哲轩用一张示意图重新定位：所有数学任务中，人类只覆盖一个蓝色椭圆，数学 1.0 就是这个椭圆的前沿；AI 则任务分化——做不了演讲（没有实体）、书面阐述不如人类，却在另一些任务上远超人类。他批评最流行的用法——把喜欢的题丢给 AI 问能不能解，是「缺乏想象力的用法」；数学任务本就多样：解题、讲解、提出新问题。
第一个实验是约两年前启动的概念验证项目：生成 2200 万道代数等式问题，每题只有真假两答，单题代数研究生约半小时可判定，但「我有 2200 万道题，可没有 2200 万名研究生」。他招募约 50 名志愿者众包，因当时现代 AI 不成熟、成本过高，改用旧式 AI（自动化定理证明）加纸笔创造性工作，最终建成大型数据集、发现构造代数结构的新方法与新类型数学，并发明了新编码「magma 同调」。海量答案还倒逼形式化——「我总不能批 2200 万份答案」。
第二场是在 L 函数模形式数据库（LMFDB）上的竞赛，形式像寻彩蛋：25000 种「花纹」即伽罗瓦群，散布的彩蛋是多项式，任务是每种花纹凑齐一枚。赛前仅约 60 种被找到过；三个月里，有人用 AI、有人用计算机代数软件、有人只用纸笔，最终全部集齐，攒出一份此前根本「收不齐」的完整数据集。实验性数据收集，正成为一类新的数学活动。
图：演讲现场 · 等式理论项目（2200 万道代数问题）
本节要点：先造数据、再做数学成为可能——2200 万道题教会 AI 与人类如何合作；LMFDB 竞赛三个月把伽罗瓦群样本从 60 种推到 25000 种。
理解了才算解对：应用数学的暗礁
纯数学自带可持续循环：有趣的问题源源不断，练「玩具问题」练出的本事经教材与讲解传下去，最终解决现实问题。循环能运转，靠的是客观可验证：答案非对即错，没有跑偏的奇异解。
应用数学麻烦得多：它和现实打交道，解出的题未必是你想要的题。天气建模是典型——用今天的模型和数据外推四天后的预测，数学上或许漂亮，但数据缺漏、模型没抓准物理规律时，一遇边缘情况就翻车。数学 1.0 时代这不成问题：人解题时既懂模型、也懂背后的真实意图，不会钻空子做出纸面好看、目标却错的答案；P 值造假偶有耳闻，但好好干本就比造假容易。
真正的危险是用错地方。AI 极擅长纯数学，恰因答案可客观验证，能海量产解；但当下模式是「用洞察力换答案」——解到手了，你却看不懂它怎么来的。以往遇到突破，他能打电话请当事人来讲透；OpenAI 那三百篇论文，却没人可聊。人类理解力曾是解题的自然副产品，正在流失。
恶果之一：历史上第一次，数学缺题可解。过去解出一道好题，往往自然带出两三道新题；AI 虽能随机生成 2200 万道题，绝大多数却没意思——研究能有所得的好题正在耗尽。更微妙的是数学家开始藏题：怕想法刚公开就被喂给前沿模型抢发，陶哲轩团队自己也藏了一批。
而最糟的不在数学之内，而在数学之外：AI 很快会被用于给电网、交通调度、药物设计、芯片设计等现实系统建模，人们大概率会照搬数学领域的做法——只管输入提示词、不懂背后原理，然后采用仅「技术上验证通过」、实则钻了模型空子的解法。AI 恰恰更擅长作弊：它被训练来给猜想找反例，同一能力让它专挑科学模型的弱点。问题不在 AI 本身，而在被用错。
图：演讲现场 · 数学 1.0 的「可持续循环」：解题 → 理解 → 外溢回应用
本节要点：纯数学对错分明，应用数学却要人理解现实；不加理解地把 AI 用在天气、电网、药物设计上，会得到「验证通过、其实解错题」的答案。
数学 2.0：让 AI 加强理解，而不是替人思考
陶哲轩用两根轴给学科定位：一轴是理解程度，一轴是技术用量。学科起步是「前数学」，理解原理、找到模型后进入数学 1.0；眼下我们正漂向「不对齐象限」——技术拉满、理解归零，把思考外包给 AI，也放弃了「这个解真是我们想要的」的保证。
出路是数学 2.0：数学 1.0 与 AI 本不必互斥，关键是不用 AI 取代理解，而是支持和加强理解。新活动已在铺开：
- 开放阐释问题：定理已证、证明却像从帽子里变出兔子——太长、依赖重型工具、缺动机。一个月后加州理工将用开源模型做大实验，专改这类证明。
- 活的网络：把逐篇积累的论文升级为实时更新的网络，而非以年为单位堆积。
- 共享大库：扩建 Lean、Mathlib 这类收录几十万条一致定理的形式化大库。
- 数学马拉松：下周学生组队去啃「完全看不懂证明」的惊人成果（含 AI 新进展）。
- 给 AI 挑毛病：数学为交通、物流、药物研发建模，模型向来有弱点，过去没有技术能主动攻破，现在有了——正好用来检测对齐何时失效。
| 维度 | 数学 1.0 | 数学 2.0 |
|---|---|---|
| 核心目标 | 攻克公开难题 | 扩大前沿、弱化解题中心地位 |
| AI 的角色 | 解出更多证明 | 加固每一环的人类理解 |
| 成果形态 | 单篇论文、逐年堆积 | 多论文「活的网络」实时更新 |
| 证明标准 | 能证出就行 | 开放阐释：可读、可复现、有动机 |
| 稀缺资源 | 时间与人力 | 想象力 |
图：演讲现场 · 数学化的四种类型：从「前数学」到「不对齐」再到数学 2.0
本节要点：数学 2.0 不是在解题上更进一步，而是把 AI 接到「理解」的每一环；瓶颈不是算力与技术，是想象力。
图：金句卡 · 证明过剩的时代
「我有 2200 万道题，可没有 2200 万名研究生。」 「只从推特获取信息，看到的往往不是真实世界。」
总结要点
- 纯数学解题恰好集齐机器学习三要素（可验证、可数字化、高质量数据），AI 因此突然擅长解题，数学进入证明过剩时代。
- 证明过剩让「解题」这个代理指标失效：答案变便宜，理解变稀缺，目标开始错位。
- 两场实验给出路径：2200 万道代数题证明「先造数据」可行；LMFDB 竞赛三个月把伽罗瓦群样本从 60 种推到 25000 种。
- 应用数学的暗礁是不理解模型就用 AI：天气、电网、药物设计会出现「技术上验证通过、实际上解错题」的答案。
- 数学 2.0 的抓手：开放阐释、活的论文网络、Lean/Mathlib 大库、数学马拉松、分析奖励模型的失效模式。
迁移与启发
- 职场：当 AI 让「产出」变得廉价，稀缺的是陶哲轩说的「理解」。别只堆交付数量，练审计与解释 AI 输出的能力——能指出模型哪里会失真的人，比单纯会用模型的人更值钱。
- 投资理财：看不懂的策略别重仓。任何「从帽子里变兔子」的量化模型或 AI 选股逻辑，先给自己设一道失效检测题：它在什么市场环境下会失效？答不上来，就降仓位。
- 生活决策：定期自查是否困在「1.0 思维」——当衡量标尺（学历、头衔、论文数）本身在贬值，敢不敢换一套玩法？先问自己：如果工具不再是瓶颈，我会做哪件不一样的事？
一句话升华
工具终将替我们完成证明，但只有想象力能替我们提出值得证明的问题。