陶哲轩：数学正进入“工业时代”MIT科技评论
7 月 24 日，菲尔兹奖得主陶哲轩（Terrence Tao）在美国费城举行的 2026 年国际数学家大会（ICM）上发表公众演讲，题为《人工智能时代的数学》（Mathematics in the age of AI）。
他没有从 AI 又解决了哪一道数学难题讲起，而是把时间拨回到 20 世纪初。
在陶哲轩看来，20世纪初，伴随着罗素悖论、哥德尔不完备定理等一系列发现，数学家被迫重新审视集合、无穷、公理等最基础的问题。这场被称为“数学基础危机”的思想震荡，一度引发激烈争论，却最终推动数学建立起更加严密、统一的现代基础体系。
而今天，随着 AI 开始参与数学研究，数学或许再次站在一个类似的历史节点。不同的是，这一次受到挑战的，不再是数学理论的基础，而是数学共同体长期默认的研究方式和价值体系：什么才算一项真正完成的成果？数学研究的目标，是尽可能证明更多定理，还是帮助人类建立更深刻的理解？
尽管陶哲轩并没有在演讲中直接使用“工业化”来形容数学的未来，但他描绘的图景已经呈现出鲜明的工业特征：数学知识将从稀缺走向充裕，研究流程被拆解为生成、验证、解释、评审和知识整合等多个环节，人类与 AI 也将在其中重新分工。当证明越来越容易获得，真正稀缺的，应该是是提出问题、理解问题，以及组织知识的能力。
（截至发稿，演讲视频尚未上线，本文主要依据陶哲轩会后发布的 52 页演讲幻灯片进行整理解读。）
真正的问题，已经不是 AI 会不会做数学
在演讲一开始，陶哲轩提出了一个“AI 能力猜想”（AI Capability Conjecture）：未来，AI 可能在可接受的成本和一定程度的人类监督下，完成部分研究级数学工作。至于它能处理哪些问题、需要多少人工参与、达到怎样的正确率和结果质量，都可以有不同设定，因此这一猜想也有强弱之分。
如果连最弱的版本都无法实现，数学界大可以延续原有的研究方式；如果较强版本成为现实，尤其当数学共同体仍把“尽可能多地解决未解问题”放在首位，现有的文化、评价体系和研究实践都将受到冲击。
陶哲轩真正关心的，是这种变化会把数学带向哪里。他在幻灯片中明确说明，这场演讲无意判断“AI能力猜想”是否成立，而是请听众先接受一个工作假设（Working Hypothesis）：假设 AI 很快能够以可接受的成本和监督，承担相当一部分研究级数学任务，数学共同体该如何应对？整场演讲由此展开，重点落在能力提升之后的制度与价值问题。
至于 AI 是否已经接近这一阶段，陶哲轩引用了一项自己参与发起的最新评测项目 First Proof 作为背景。
今年 5 月底，First Proof 在严格控制的条件下测试了四套 AI 数学系统。10 道此前从未公开的新题全部来自真实研究过程，由相关领域专家按照学术期刊的审稿标准，对解答的正确性和论文表述进行评估。结果显示，四套 AI 系统共在 10 道题中成功解决了 7 道，每道题至少有一份解答达到学术期刊发表水平，单题计算成本约为 10 至 1000 美元。
但这项评测中也暴露出了 AI 的局限。虽然它已经能够完成研究级证明，却仍会出现引用错误、解释不足等简单错误。在介绍 First Proof 之前，陶哲轩还特意提醒，当前许多关于 AI 数学能力的公开案例都存在报告偏差（reporting bias），算力投入、人工参与和失败案例等关键变量往往没有完整披露，因此现有材料还不足以支撑稳固判断。
这不禁让人联想到在 ICM 开幕前几天，数学界还发生了一个引发热议的事件。7 月 20 日，Anthropic 数学家 Levent Alpöge 公布了一个由 Claude Fable 5 参与发现的雅可比猜想三维反例。随后，研究者利用 Isabelle/HOL 完成了形式化验证，确认这一反例成立。
证明很快得到了验证，但新的问题随之出现：它为什么成立？这样的构造是如何想到的？
第二天，陶哲轩在个人博客发表长文，对这一反例进行了详细解读。他不止停留在验证结果，而是一步步还原其背后的几何构造，解释它为什么成立，以及它与已有理论之间的联系。
某种意义上，这正是他在 ICM 想讨论的事情。当机器越来越擅长生成和验证证明之后，人类数学家的工作不会随之结束，而是转向另一件同样重要的事情：解释证明、组织知识，并帮助数学共同体真正理解这些成果。
而要理解这种变化，就必须先回答一个更根本的问题：数学共同体究竟希望数学研究实现什么？
从“证明稀缺”走向“证明过剩”
在陶哲轩看来，数学研究从来不只有“解出更多题目”这一个目标。它同时承担着许多不同的使命：解决未解问题、发展新理论、理解世界、建设共同体、培养下一代数学家、扩展共享知识，以及创造具有持久审美价值的作品。
过去，这些目标大体是正相关的。解决重要问题往往意味着发展新理论；寻找证明的过程，也会培养年轻数学家、丰富数学共同体。因此，“解出了多少问题”“谁最先证明”，在相当长时间里都可以近似代表更复杂的学术价值。
但 AI 可能即将打破这种关系。
陶哲轩借用了经济学中的古德哈特定律（Goodhart's Law）：当一个指标成为优化目标，它就不再是一个好的指标。生成式 AI 缺少现实世界的约束，AI 公司又有展示模型能力的动力，因此尤其容易把“解出更多数学问题”这一指标推向极致。
图｜古德哈特定律：优化指标，不等于实现目标。（来源：Image 2）
为了说明这一点，陶哲轩在演讲中围绕“一个数学问题究竟何时才算真正解决”展开了五层递进的讨论。
在最初，数学家们的目标只是“尽可能多地解决未解问题“。但这样的标准很容易产生大量错误证明，于是第二层需要加入验证（verification）。
不过，随着 AI和自动形式化（autoformalization）的发展，证明生成（proof generation）和证明验证（proof verification）都在迅速加快。Rocq、HOL、Lean 等证明助理已经能够逐步检查形式化证明。但新的问题也随之出现：如果机器生成了一份已经通过验证、却没有任何人真正理解的证明，它是否意味着这个数学问题已经真正解决？
陶哲轩给出的答案是否定的。因此，第三层进一步加入了阐释（proof exposition）：证明不仅要正确，还需要有人解释它为什么成立、有什么意义。而如果再往上一层，成果不止停留在个人，还需要获得数学共同体的认可，其他研究者不仅确认结论正确，也能够理解其中的方法，并将其应用到新的研究中。最后，它还需要进入标准理论、教材和数学共同体共享的知识体系，成为后来者继续发展的基础。
一条完整的知识链出现了：开放问题首先变成未经核验的证明，再经过验证、阐释、同行接受和知识整合，最终才成为稳定的数学知识。
图 ｜陶哲轩提出“数学问题真正解决”的五层目标（来源：陶哲轩）
AI 可以大幅提高这条知识链前端的生产效率，却无法自动扩建后端。等待验证、阐释和整理的证明会越来越多，论文不断挤压同行评审系统；即使最终发表，数学界也未必有足够的人力和时间，把这些成果真正吸收、消化，并整合进成熟的理论框架。
陶哲轩把这种错配比作一种“证明的消化不良”（proof indigestion）。数学或许将从一个证明稀缺的时代，进入一个证明过剩的时代。
这也延续了他近几年的判断。2023 年 6 月，陶哲轩曾预测，把大语言模型与形式化验证、检索和符号计算结合之后，2026 年左右，AI 有望成为数学研究中值得信赖的合作者。当时，他紧接着追问的就是：期刊、引用规则和研究生培养体系，该如何适应这样的变化。
到了 2026 年 6 月，他进一步提出了“Big Mathematics（大数学）”的概念：未来复杂的数学研究将被拆分成大量子任务，由分布式的人机协作网络共同完成；人类更多负责提出问题、设计方向和创造性工作，AI 则承担证明生成、形式化验证等技术性任务。
而这次 ICM 演讲，则把他的思考又向前推进了一步。真正的瓶颈，已经不再只是如何生产更多证明，而是如何验证、理解、传播并消化这些证明。数学未来需要建设的，不只是更强大的“证明工厂”，更是一套能够支撑质量控制、同行评审、知识整理和共同体传承的新体系。
答案正确，还远远不够
如今的 AI，已经可以生成语法、拼写和格式几乎无可挑剔的数学文本。但在陶哲轩看来，这类文本的阐释能力仍然参差不齐：它们往往在简单的部分停留过久，却在真正困难或新颖的地方一笔带过，也很少主动说明一项结果与已有文献之间的联系。
更隐蔽的问题，还来自过度润色。人类作者曾经觉得困难的地方，往往会保留一些思考和推导的痕迹，提醒读者放慢速度、反复推敲。过于光滑的 AI 文本，却可能把常规步骤和关键突破写得同样轻松，反而掩盖了真正值得学习和理解的思想。
陶哲轩展示了一张自己年轻时阅读法国数学家让・布尔甘（Jean Bourgain）1991 年论文的照片。纸页上写满了批注。对他而言，阅读、停顿、补全中间步骤、重新组织思路，恰恰是理解形成的过程，并不需要被完全删去。
（来源：陶哲轩）
随后，他引用了美国数学家威廉・瑟斯顿（William Thurston）1994 年关于数学证明的经典论述：数学并不是为了完成一项由定义、定理和证明组成的抽象生产指标，真正的衡量标准，是能否让人们更清楚、更有效地理解和思考数学。
证明的发表也不是终点。它还需要被共同体接受、使用，并最终成为教材和标准理论的一部分。其中最缓慢、也最容易被忽视的工作，往往由编辑、审稿人、教材作者以及负责阐释成果的数学家完成。这些工作远不如率先给出证明那样耀眼，却承担着把个人成果转化为共同知识的职责。
