7月24日，菲尔兹奖得主陶哲轩（Terrence Tao）在美国费城召开的2026年国际数学家大会（ICM）上，发表了一场题为《人工智能时代的数学》（Mathematics in the age of AI）的公众演讲。
他并未从AI攻克某道数学难题切入，而是将视线拉回20世纪初。
在陶哲轩看来，20世纪初，受罗素悖论、哥德尔不完备定理等一系列发现冲击，数学家被迫重新审视集合、无穷、公理等最底层的问题。这场被称作“数学基础危机”的思想震荡，虽曾引发激烈争论，最终却推动数学建立起更为严密、统一的现代基础体系。
如今，随着AI介入数学研究，数学或许正站在类似的历史路口。区别在于，此次受挑战的不再是理论根基，而是数学共同体长期默认的研究范式与价值标尺：何为真正完成的成果？研究目标是尽可能多证定理，还是助力人类建立更深层的理解？
图 ｜ 大会现场（来源：X）
尽管陶哲轩未在演讲中直接使用“工业化”一词描绘数学未来，但他勾勒的图景已显工业特征：数学知识将从稀缺转向充裕，研究流程被拆解为生成、验证、解释、评审及知识整合等环节，人机分工随之重塑。当证明获取日益容易，真正稀缺的，应是提出问题、理解问题以及组织知识的能力。
（截至发稿，演讲视频尚未上线，本文主要依据陶哲轩会后发布的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完成形式化验证，确认反例成立。
图 ｜ Levent Alpöge （来源：Quanta Magazine）
证明迅速获验，新问题随即浮现：它为何成立？此类构造如何构想？
次日，陶哲轩在个人博客发文，对该反例进行详细解读。他不止步于验证结果，而是一步步还原背后几何构造，阐释其成因及与已有理论之联系。
某种意义上，这正是他在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年关于数学证明经典论述：数学并非为完成由定义、定理和证明组成的抽象生产指标，真正衡量标准，是能否让人们更清楚、更有效地理解和思考数学。
证明发表非终点。它还需被共同体接受、使用，并最终成为教材和标准理论一部分。其中最缓慢、也最易被忽视工作，往往由编辑、审稿人、教材作者及负责阐释成果数学家完成。这些工作远不如率先给出证明耀眼，却承担着把个人成果转化为共同知识职责。
基于此，陶哲轩提出几项值得数学共同体重新思考方向。
首先，披露AI使用应成学术写作常态。陶哲轩即在幻灯片中注明，AI被用于文字自动补全和图表生成。
其次，评价体系或需降低对“第一个解出问题”和证明数量强调，将更多认可给予阐释、验证和知识整合工作。陶哲轩提出，若作者无法独立就研究结果作出一份清楚、准确且引用完整的专家级报告，则此项成果不应直接发表。
AI可助期刊筛除明显缺乏验证或写作质量较差论文，却无法替代数学共同体作出最终判断。一个成果是否值得进入学科主线，仍是一个缓慢、依赖专业判断和长期共识形成过程。
与此同时，数学家职业分工也已开始变化。2026年4月，陶哲轩在接受Nature采访时曾表示，数学家“工作要求正在改变”。而本届新晋菲尔兹奖得主雅各布齐默尔曼（Jacob Tsimerman）则宣布，他将在8月底加入OpenAI，从事AI安全研究，希望为多智能体系统建立更严格理论保证。
几天前借助Claude Fable 5找到雅可比猜想反例的Levent Alpöge，正是齐默尔曼曾指导本科毕业论文学生。如今，两人分别进入Anthropic和OpenAI：一位借助AI探索新数学对象，一位研究如何让更强AI更加安全可靠。
这当然不能代表所有数学家选择，但折射出一种正在发生的变化：未来数学家工作，也许不再只是生产新证明，而是设计验证体系、解释机器生成结果，并参与塑造人与AI协作新规则。
演讲之后，他让AI采访了自己
演讲结束次日，陶哲轩又做了一个有趣实验。
7月25日，他在Mastodon上透露，自己让AI汇集并整理过去发布的100多篇帖子、采访和视频，总结其对AI观点；对于已有材料未涉及问题，再由AI反过来“采访”自己。他还特意要求AI把问题设计得更尖锐一些。
图 ｜ 陶哲轩公开发布由AI主持的访谈，作为其AI观点总结补充材料。（来源：陶哲轩）
在此过程中，AI提出的许多问题，都与这场演讲形成呼应：与多家AI公司合作，是否会为行业炒作提供信誉？数学能够自动验证，是否只是一个无法推广到医疗、司法等领域的特殊样本？一边警告“证明消化不良”，一边推动大规模数学项目，是否也在加速“证明过剩”？
陶哲轩未回避这些问题。他表示，大规模项目会尽量放在长期缺乏关注的数学“长尾”问题上，避免与年轻数学家研究方向直接竞争；至于如何判断一份证明是否真正被“消化”，未来很可能需要期刊、教材和出版体系逐渐建立新规范。
某种意义上，这场自我采访，即他所倡导的人机协作缩影：AI阅读资料、寻找遗漏、提出问题、生成初稿；人类负责审阅、修正，并对最终内容负责。
从2023年预测AI将成为数学家合作者，到2026年讨论如何理解和消化机器生成证明，陶哲轩关心的问题已发生变化。AI能否参与数学研究，正逐渐从预测走向现实；数学共同体如何重新组织知识、调整评价标准、建立新协作方式，才是接下来真正需面对课题。
未来值得关注，也许不只是模型还能证明多少定理，而是期刊是否会调整审稿与披露规则，大学如何重新设计数学教育，解释、验证和整理知识工作能否获得应有价值，以及机器生成成果最终有多少能够进入教材、融入理论，并成为后来者继续发展起点。
参考链接：
1.https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf
2.https://1stproof.org/second-batch.html
3.https://1stproof.org/assets/docs/report.pdf
4.https://isa-afp.org/entries/Jacobian_Counterexample.html
5.https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/
6.https://teorth.github.io/tao-web/ai-views-interview.html
