陶哲轩 ICM 2026《AI 时代的数学》：当证明变得廉价，数学还剩什么
视频：B 站 BV11T8A6FEgC，时长约 51 分钟。B 站页面没有公开字幕，因此本文不是逐字稿，而是根据视频主题、陶哲轩的讲演论文和公开幻灯片整理出的分析。
真正的问题不是 AI 会不会做数学
如果把这场讲演压缩成“AI 能不能证明定理”，就会错过重点。陶哲轩把问题推向了数学共同体：当机器可以批量生成研究级候选证明，人类还有多少时间去阅读、验证、解释和吸收这些结果？
计算器没有让算术失去意义，计算机代数系统也没有让符号变形消失。工具每次变强，稀缺环节就会移动。AI 可能把瓶颈从“能不能写出一个看起来像证明的东西”，推到“哪些证明值得相信、值得理解、值得进入数学知识体系”。
证明不是一句话，而是一条流水线
研究数学至少包含这些环节：提出值得研究的问题，把猜想改写成可处理的形式，寻找例子和反例，生成候选论证，检查每个步骤，写出别人能复用的解释，最后让结果通过报告、引用、教学和后续工作进入共同知识。
AI 能介入其中很多环节，却不能把它们等价处理。模型可以提出引理、翻译记号、检索文献、生成 Lean 代码；定理证明器可以拒绝不合法的形式项。但“形式上正确”不等于“问题重要”，也不等于“人类理解了它为什么成立”。
所以“AI 生成了一个证明”不是完整新闻。形式验证能确认一种很强的正确性，却不会自动给出好的定义、清晰的动机、简洁的概念解释，也不会告诉我们这个结果会改变哪一部分数学。
证明越多，注意力越稀缺
生成十个候选证明时，研究者还可以逐个阅读。生成一万个之后，生产就不再是瓶颈，验证、排序和解释才是。
这和 Goodhart 定律有关：一个指标一旦成为目标，系统就会优化指标本身。假如论文数量、证明长度或基准分数成为主要奖励，研究者可能得到大量技术上成立、却没有长期价值的论证。
数学的目标本来就不止“解决更多开放问题”。它还包括建立理论、理解现象、训练下一代、维护共同体，以及创造能够被后人使用的知识。“定理更多”只是一个指标，而且很容易失真。
最现实的风险不是正确数学突然变成错误数学，而是新材料的涌入速度超过共同体的辨别能力。
形式化验证是连接人和机器的桥
自然语言证明短小灵活，却包含大量省略步骤、上下文和默认记号。Lean 这类系统要求把定义、依赖和证明对象写成机器可检查的形式。
形式化不一定只是论文完成后的审计。它可以成为人和模型之间的接口：模型提出证明状态或 tactic，证明器立即反馈哪些部分被接受，研究者再调整命题、策略或拆分方式。相比聊天式回答，这种反馈范围更窄，但更精确。
代价同样明显。形式化一个定理有时比写非形式证明耗时更长，尤其是在库里没有合适抽象时。形式证明也可能很难读懂。合理的工作流应当分层：用自然语言和计算实验快速探索，用形式系统检查可靠性，再由人写出能传递思想的解释。
AI 会让合作更大，也更复杂
数学从来不是完全孤立的个人劳动。它依赖讨论、例子、引用、软件、数据库、报告和共享记号。AI 只是让这种合作变得更明显，并且可能扩大到无法靠传统署名规则描述的规模。
一个人让模型搜索猜想的变体，另一个人把幸存的引理形式化，第三个人找出反例，第四个人把结果写成可读的文章。于是作者资格、错误责任、工具版本、提示词和失败记录都会变成学术记录的一部分。
公开说明工具使用情况不是形式主义，而是溯源。读者需要知道哪些内容由模型生成、哪些内容经过证明器检查、哪些内容由人重新组织。否则，未来的人无法判断结果是否能独立理解、能否复现，以及它是否依赖某个已经消失的服务。
学生应该学会质疑工具
模型最危险的地方不是总会答错，而是能在学生还没有学会检查假设时，给出非常顺滑的答案。
与其简单禁用，不如把 AI 当成对抗性伙伴：要求它给出多种方法，逐一核对假设；先让它找反例，再接受一般命题；把小引理交给形式化系统；关掉生成内容后自己重述证明；记录失败路线以及失败原因。
AI 时代更值钱的能力不是记住每一个变形步骤，而是判断：哪个问题值得问，哪一步可疑，某个抽象为什么应该存在，以及如何把一条长证明讲给别人听。
我的判断：变化首先是制度性的
AI 不会同时改造所有数学领域。形式库丰富、结构清晰、验证成本低的方向更容易受影响；依赖新定义、几何直觉、长期文化背景和研究品味的方向，变化可能更慢。同一个领域内部也会很不均匀：系统可能证明一个看起来困难的技术引理，却在简单变体上失败。
因此，最值得采用的评估单位不是“模型会不会做题”，而是一整条流程：问题选择、候选生成、检查、解释、复现和后续使用。
这场讲演最重要的提醒，是数学共同体应该在机器用数量迫使它做决定之前，先说清楚自己珍惜什么。AI 可以生成候选，证明器可以检查义务，但人仍然要决定什么算进步、什么值得解释、什么应该被传给下一代。