从证明生成到数学消化：陶哲轩谈AI时代的数学
2026年7月24日，陶哲轩在国际数学家大会的报告《Mathematics in the Age of AI》中[1-2]，对AI时代的数学工作进行了探讨。他设定了一个工作假设：不久以后，AI可以在一定成本和人工监督下，完成相当一部分研究级数学任务。随后，他集中讨论数学共同体的目标、价值和工作规范。
陶哲轩没有要求听众相信或期待这个假设成真。目前用来判断AI数学能力的案例大多没有在统一条件下测试：模型调用次数、人工介入程度、计算费用和失败尝试常未完整披露，企业又更愿意发布成功结果。不同案例因此难以放在同一尺度上比较。他暂时接受一个较强假设，用它检验数学研究原有的评价方式[1]。
AI会拆开过去捆在一起的目标
数学研究同时追求很多东西：解决问题、发展理论、理解世界、建设共同体、训练下一代、扩展公共知识，也包括创造具有审美价值的作品。过去，这些目标通常互相带动。解决一道困难问题往往伴随新方法、研究训练、同行交流和理论整理，所以“解决了多少问题”“发表了多少定理”尚可充当数学进步的近似指标。
AI可能使这些目标分开。一套系统可以生成正确证明，却没有训练任何数学家；可以解决一个问题，却没有形成能够复用的理论；可以写出语法完整的论文，却没有标出论证中最困难的部分。产出数量继续增加，数学理解未必同步增长。
陶哲轩借古德哈特定律说明这种风险：一个指标受到过度优化后，便会失去原有的衡量作用。用工程语言说，AI提高了整个系统的优化能力，原来含糊的目标函数随之暴露。数学共同体如果仍然主要奖励证明数量、论文数量和最先完成者，模型就会不断推高这些代理指标，验证、理解、训练和共同体记忆则可能停在原处[1]。
陶哲轩把这次变化与20世纪初的数学基础危机相提并论。这个类比有明确限度。今天没有出现类似罗素悖论那样动摇数学一致性的矛盾，受到冲击的是数学实践中长期保持隐含的价值判断：成果如何定义，作者承担什么责任，什么内容值得发表，哪些结果应当进入教材[1]。
制度问题由此出现：可计数的证明和论文仍被奖励，理解、训练和共同体记忆却没有同步增长。
一份证明离数学知识还有多远
陶哲轩用一组不断扩展的流程图组织报告。开放问题先得到候选证明；候选证明随后经历正确性验证、清楚表达、同行接受和理论整理，最后才可能成为教材、参考资料或工具库中的标准知识[1]。
开放问题 → 候选证明 → 验证 → 表达 → 同行接受 → 纳入标准理论
传统叙述常在“证明完成”处结束。陶哲轩把“证明完成”这个节点放在流程前半段。证明需要专家检查，也需要作者说明关键思想、已有文献和适用范围。同行还要使用、修改和传播这项结果。经过一段时间后，少数结果会被压缩成标准引理、方法或教材章节[1]。
这几道工序的速度并不相同。AI提高候选证明的到达速度，形式证明助手也加快了部分验证工作；阅读、审稿、解释和理论整理仍然依赖有限的专家注意力。候选证明的到达速度超过共同体的处理速度，积压便会出现：
- 未验证的证明等待专家检查；
- 已验证的证明等待可读的说明；
- 写成论文的结果挤压审稿系统；
- 已发表的结果等待整理，长期停留在彼此孤立的状态。
陶哲轩把这种积压称为“证明消化不良”。数学可能由证明稀缺进入证明过剩。此后更稀缺的资源包括可信的专家时间、准确的解释、可靠的引用、对问题重要性的判断，以及把零散结果组织成理论的能力[1]。
陶哲轩引用的First Proof第二批评测给出了一组接近研究现场的数据。评测选择10道未公开的研究级问题，在受控条件下测试4套AI系统，再由领域专家盲审正确性和表达质量。评测结果显示，其中7道题均至少有一支团队给出了达到可发表水平的解答，单题计算成本约为10至1000美元。这个结果说明研究级证明的生成成本已经可以降到相当低的范围；它同时留下了审稿、复核和归属问题[3]。
这组数据暴露了成本转移：机器以10至1000美元生成候选结果，同行仍要承担审稿、复核和归属判断。
求解提速如何改变证明流程
First Proof展示了研究级任务的总体结果，其他案例则分别显示预处理、验证、解释和规模化搜索发生了怎样的变化。
2024年，DeepMind的AlphaProof和AlphaGeometry 2在国际数学奥林匹克竞赛中解出6道题中的4道，得到28分。题目需要专家先翻译成Lean等形式语言，计算持续两三天[4]。2025年，Gemini Deep Think解出5道题，得到35分；系统直接读取自然语言题目，在4.5小时竞赛时限内生成自然语言证明[5]。两次结果之间的差别不只是一道题。人类原先负责的形式化预处理和结果转换已经被系统吸收进流程。
IMO仍属于边界清楚的封闭任务。题目短，答案确定，不要求系统选择研究方向，也不要求它把结果放进长期文献。因此，竞赛成绩适合说明求解能力的变化，无法单独说明系统已经完成数学研究的全部工作。
2026年5月，OpenAI公布了一项平面单位距离结果。内部模型生成了反驳Erdős相关猜想的构造，外部数学家随后检查证明，并撰写配套论文补充背景和解释材料。机器给出了结果，专家的工作说明这一构造使用了哪些结构，以及代数数论方法为何会进入离散几何[6]。
同年7月，Fable AI给出三维雅可比猜想的反例。显式映射写出后，检查雅可比行列式和非单射性只需要较短计算，公式的来历却难以理解。陶哲轩随后写了一篇反例的“消化”[7]，把公式放回多项式乘法、局部可逆性和仿射切片的几何结构中。验证确认了反例成立；消化工作解释了人类能够从反例中带走什么。
Equational Theories Project展示了另一种规模。项目处理4694条较短代数恒等式之间的22,028,942个蕴含关系，结合穷举、自动定理证明、人类构造和Lean形式化完成整个图谱。海量蕴含关系得到判定后，研究任务转向压缩规律、寻找不变量和组织一般构造[8]。
这些案例处在不同层级，不能合并成一条简单的能力曲线，但仍表明求解和验证正在提速，解释、筛选和理论组织所需的工作量随之增加。
数学消化包含哪些工作
这里的“消化”指共同体把一份已验证结果转化为可理解、可引用、可复用知识的过程。它涵盖几种不同的劳动。
压缩要求从长篇推导中找出决定结果的机制。定位要求区分常规技术、关键步骤和可能推广的部分。连接要求说明新结果与已有文献、相邻领域和旧方法的关系。迁移则把一次性的证明改造成引理、框架、算法、反例生成方法或可供教学的理论。
正确证明仍然可能没有得到充分理解。形式证明助手检查的是符号推导在给定公理、定义和命题下能否成立。形式化命题是否准确表达原问题，仍需数学家负责判断。软件通过测试可以证明它符合现有测试，无法证明需求本身写对了；形式验证也存在相似边界。
陶哲轩还讨论了“过度顺滑”的证明。人类作者会在困难处留下某种阻力：解释加长，符号推导放慢，或提醒读者停下来。AI可能把常规步骤和关键步骤写得同样工整，语言更整洁，难度信号却消失了[1]。
陶哲轩把摩擦分为两类。机械重复、格式转换和冗长计算可以交给工具；概念障碍、路线选择和暂时的不理解构成学习与发现的一部分。去除前一类摩擦能够节省时间，遮住后一类摩擦会妨碍读者识别证明的关键位置[1]。
这也解释了AlphaGo类比的限度。围棋有清楚的终局判定，一手棋提高胜率就具有明确价值。数学还要检查一项结果依靠什么结构，能否推广，是否改变旧问题的理解，以及后来的人能否继续使用这种方法。AlphaGo只需要赢。数学还要形成棋理。
重新计算学术劳动的价值
现有学术制度把发现者、第一作者和率先解决问题的人放在显眼位置，验证、审稿、重写、维护数据库和整理教材通常得到较少声望。候选证明的生产成本下降后，这种排序会把成本转移给编辑、审稿人和读者。作者可以迅速提交长稿，领域专家仍需花费数天或数周判断其正确性和价值。
陶哲轩据此建议降低对证明生成和“第一个解决者”的强调，提高对解释、发表组织和标准化工作的评价。他提出一条经验规则：作者如果无法就结果作一场清楚、正确、引用规范的专家级报告，这项结果不应发表。这里需要检查的是作者能否说明关键思想、回应实质问题并承担错误责任。报告是否漂亮不适合作为新的代理指标[1]。
《莱顿人工智能与数学宣言》把部分责任写成制度建议：披露自动工具的使用，保留人类作者对正确性和引用的责任，帮助审稿人复核，在条件允许时提供形式证明和可复现材料。AI可以参与写作和求解，人类作者仍需对发表行为负责[9]。
教育需要另一套边界。研究者掌握基本能力后，可以用AI处理计算、代码、文献初筛、形式转换和反例搜索。学生手算、试错、写错证明和重新组织概念，本身就是训练过程。陶哲轩因此主张在教育和训练中强调人的参与，并严格限制部分AI用途。工具省下多少时间并非唯一尺度，还要看它是否拿走了原本需要形成的能力[1]。
总结与讨论
陶哲轩的报告给出了讨论框架，但共同体判断的局限、AI参与“消化”的可能性，以及评价标准的适用边界，仍需进一步讨论。
共同体接受缓慢且依赖人类，这个事实不能证明共同体的判断天然可靠。声望、学派、语言、地区和审稿资源都会影响结果的传播。形式验证完备的匿名贡献，有时可能比依赖熟人信用的传统论文更容易检查。AI与形式证明也可能扩大数学研究的参与范围。
AI也未必长期停留在证明生成和形式验证阶段。它已经参与文献联系、证明压缩、类比解释和结构归纳。陶哲轩发布的观点摘要和配套访谈讨论了证明“消化”的评价标准，以及AI参与相关工作的边界[10-11]。以后相当一部分“消化”工作也可能由机器完成。难点会进一步移动到解释的选择：哪些联系值得保留，哪一种说明应当进入领域的标准叙述。
近期案例还带有明显的不确定性。公司发布成功结果时具有传播动机，失败尝试和完整成本较少公开。First Proof采用独立选题，预先规定测试条件，公开测试日志，并由专家盲审；相比单独展示成功案例，这种评测更适合判断系统能力[3]。陶哲轩同样将报告偏差和非科学激励列为当前证据的两项问题[1]。
将“作者能否作专家报告”作为判断标准时，需要避免它演变成新的表达能力测试。研究者可能使用非母语，也可能不擅长公开讲解。责任应落在数学内容上：作者能否解释关键步骤、回答同行质疑、说明引用关系，并在结果出错时承担责任。
陶哲轩没有提供完整的制度方案。他把长期被视为附属劳动的环节放回数学研究的中心：验证、解释、审稿、同行使用和教材化决定了一项个人成果能否成为共同体知识[1]。
AI继续降低证明生成成本后，问题定义、结果检查、理论组织和责任归属会占据更多时间。数学界需要调整奖励方式，也需要建设新的验证与知识整理基础设施。一个正确证明只表示结果进入了流程。
参考文献
[1] TAO T. Mathematics in the age of AI: public lecture, International Congress of Mathematicians 2026[EB/OL]. (2026-07-24)[2026-07-25]. https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf.
[2] DUONG Y. AI will be top of mind at ICM, math’s biggest conference[EB/OL]. (2026-05-04)[2026-07-25]. https://www.simonsfoundation.org/2026/05/04/ai-will-be-top-of-mind-at-icm-maths-biggest-conference/.
[3] ABOUZAID M, SRIVASTAVA N, WARD R, et al. First Proof Second Batch[EB/OL]. (2026-06-16)[2026-07-25]. https://doi.org/10.48550/arXiv.2606.18119.
[4] ALPHAPROOF AND ALPHAGEOMETRY TEAMS. AI achieves silver-medal standard solving International Mathematical Olympiad problems[EB/OL]. (2024-07-25)[2026-07-25]. https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/.
[5] LUONG T, LOCKHART E. Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad[EB/OL]. (2025-07-21)[2026-07-25]. https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/.
[6] OPENAI. An OpenAI model has disproved a central conjecture in discrete geometry[EB/OL]. (2026-05-20)[2026-07-25]. https://openai.com/index/model-disproves-discrete-geometry-conjecture/.
[7] TAO T. A digestion of the Jacobian conjecture counterexample[EB/OL]. (2026-07-21)[2026-07-25]. https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/.
[8] BOLAN M, BREITNER J, BROX J, et al. The Equational Theories Project: advancing collaborative mathematical research at scale[EB/OL]. (2025-12-16)[2026-07-25]. https://doi.org/10.48550/arXiv.2512.07087.
[9] Leiden Declaration on Artificial Intelligence and Mathematics[EB/OL]. (2026-06-02)[2026-07-25]. https://doi.org/10.5281/zenodo.20302944.
[10] TAO T. Terence Tao on AI in mathematics (and beyond)[EB/OL]. (2026-07-24)[2026-07-25]. https://teorth.github.io/tao-web/ai-views.html.
[11] TAO T. Interview: Terence Tao on AI[EB/OL]. (2026-07-23)[2026-07-25]. https://teorth.github.io/tao-web/ai-views-interview.html.