陶哲轩：AI 证明泛滥，正在把数学与人类理解割开

周五晚上在加州理工学院的一场公开讲座上，陶哲轩 —— 公认在世最有成就的活跃数学家 —— 告诉听众，人工智能已经永久终结了那个时代：产出数学证明稀少、艰难、依赖杰出的人类专长。他认为，这个终结并不代表数学的胜利。它代表一种紧迫的结构性风险，并要求重新思考数学研究究竟是为了什么。

陶哲轩把正在成形的框架称为「数学 2.0」。这场一小时的演讲是加州理工 AIM 公开讲座系列的一部分，阐述了为什么 AI 发现数学格外好对付，为什么主流的机构反应 —— 争先恐后地更快解决更多未解问题 —— 恰恰是错的，以及数学中富有成效的人机协作可以是什么样子，并以进行中的项目作为「数学 2.0」已在建设之中的证据。

让数学成为 AI 最好对付的领域的三个性质

陶哲轩的论证从一个结构性诊断开始。数学有三个性质，合在一起几乎完美契合现代机器学习系统最擅长的事。

第一是客观可验证。一个数学证明要么成立要么不成立，而这可以机械化。交互式定理证明器 Lean让计算机能检查一个形式化证明在其公理系统内是否逻辑自洽。证明在 Lean 中通过验证，其正确性就有了保证，无论是否有人理解它 —— 这把专家判断的瓶颈从评估中拿掉了，让 AI 生成的数学可以以生物学或化学里不可能的方式规模化。

第二个性质是完全可数字化。数学证明不需要物理装置、实验室设备或真实世界的数据。一个证明助手、一个标准定义库和算力就够了。

第三是规模化的高质量训练语料。几乎所有重要的二十世纪数学都已数字化。arXiv 预印本服务器收录了超过 240 万篇论文；Lean 的 Mathlib 库以机器可验证的形式形式化编码了数十万条大学水平的定理。这是一个在质上比多数科学领域干净得多的训练分布。

这些性质合在一起构成一个近乎理想的强化学习反馈回路，解释了为什么领先的 AI 实验室把不成比例的算力投向数学推理基准。

被 AI 打乱的证明稀缺生态

要理解证明泛滥为什么危险，得先理解证明稀缺建立了什么。大约一个世纪以来，数学的整套机构体系建立在一个基础假设上：为重要问题生成正确证明极其困难、极其罕见。同行评审、终身教职结构、奖项竞赛和发表渠道，全都按这种稀缺校准。

解题从来不是数学的真正目标。陶哲轩说得很明白。真正的目标是人类对数学结构的理解 —— 洞察结果为什么成立、不同领域如何相连、哪些工具可以推广。解题曾是理解的一个可靠代理指标，因为在一个只有真正的领悟才能成功证明的世界里，解决难题是深厚知识的有力证据。

AI 打破了这个代理关系。系统现在能为曾需要专家多年努力的问题生成形式化验证过的证明。它们并不总是 —— 或许通常不会 —— 产出那条可理解的推理链，让数学家得以提取并在其上构建底层的洞见。陶哲轩认为，把 AI 优化成更快解决更多未解问题，会切断证明与理解之间的联系，从而主动伤害数学。

幸存者偏差与参差不齐的能力轮廓

陶哲轩用一个二战的类比说明高估 AI 数学能力的危险。分析人员研究受损返航的轰炸机，看到损伤集中在机翼和机身，发动机相对完好。本能的反应是加固那些部位。Abraham Wald 意识到，损伤图显示的只是飞机被击中后还能幸存的部位 —— 发动机中弹的飞机根本没能飞回来被统计。

关于 AI 数学进展的新闻稿和社交媒体有着同样的幸存者偏差。成功的证明被宣布；失败的尝试无人报道。结果是一幅系统性失真的图景。

而First Proof 基准，一个由独立研究者运行的外部评测项目，提供了一个矫正。从贡献者正在进行的研究中选出的问题被拿来测试 AI 系统，由独立评审评估结果。这个基准的设计 —— 包括 AI 系统未能以可发表质量解决的问题 —— 正是新闻稿式报道所遗漏的诚实记账。

延伸阅读：OpenAI 称已解决百余道数学难题，验证还在路上

底下的模式就是陶哲轩所说的 AI「参差不齐」的能力轮廓：在客观可验证、封闭、可数字化的领域里表现出色；在需要主观判断、物理世界交互或真正开放式发现的情境中则脆弱得厉害。这个轮廓不规则，容易被误读为均匀的能力。

已经在运转的「数学 2.0」项目

陶哲轩把「数学 2.0」呈现为对正在进行的工作的描述，而不是一种愿景。

其中，等式理论项目是最清楚的概念验证。这个项目于 2024 年 9 月作为一次众包的 Lean 4 协作启动，目标是对幺半群上 4694 条等式定律中的每一对，判定一条是否蕴含另一条 —— 总计 22028942 个蕴含关系。2025 年 4 月 14 日，项目宣布完全闭合：每个蕴含关系都已判定，每个证明都在 Lean 中验证。这个结果不是某一家 AI 实验室的成就。它是以穷尽地理解一个有界领域为目标的、分布式的人机协作。

其次，逆伽罗瓦问题挑战（IGP24）于 2026 年 6 月作为第三届 SAIR 竞赛启动，针对一个经典的未解问题：是否每个有限群都是有理数域某个扩张的伽罗瓦群。第一阶段的目标是给出实现全部 25000 个 24 次伽罗瓦群的显式多项式，提交于 2026 年 8 月截止。第二阶段现在瞄准 31 次。这个项目体现了「数学 2.0」的模式：AI 让单个研究者不可能完成的全领域普查成为可能。

开放阐释问题把 AI 的任务整个重新框定。目标不是解决未知的问题，而是为已知正确的结果找到更好的证明 —— 更初等、更直观、更可迁移。加州理工 Mathathon，一场将于 2026 年 11 月 13 日至 15 日举行的学生竞赛，将用 AI 为已确立的结果寻找新证明，包括四色定理和纳维-斯托克斯方程的若干方面。这项活动「老问题，新证明」的形式，是在此前一个开放问题的设计招致数学家强烈批评之后，根据社群反馈定下的。消融研究把这一思路再推一步：从一个现有证明里拿掉一个强力工具，问 AI 结果是否还成立。放宽一个假设，看哪些推论还保留。产出的是对该定理数学邻域的理解，而不是一个上头条的解答。

支撑性的基础设施包括显式解析数论集成网络—— 一张活的、可查询的、相互关联的解析数论结果表 —— 以及 Mathlib 的持续扩充。陶哲轩指出，开源的数学 AI 模型预计即将发布，这将降低研究者和学生的准入门槛，不必依赖专有的实验室系统。

形式化验证还不够时：纯数学中的对齐风险

陶哲轩最尖锐的论点，关乎 AI 生成形式上正确、人类却不理解的答案时会发生什么。他提出一个思想实验：一个 AI 系统受命寻找一种能通过某种癌症三期临床试验的药物。系统合成了一个新分子，构建了一个预测疗效的数学模型，在 Lean 中验证了预测，药物也真的通过了试验。没有人理解其机制。

你会注射它吗？

陶哲轩的回答：不会 —— 因为 AI 可能利用了临床试验结构中的某个人为缺陷，满足了形式规范却错过了真正的目标。一种机制不透明的疗法无法安全地推广、调整或与其他疗法联用。形式化验证证明的是系统内部的逻辑一致性。它不证明规范抓住了任何人真正想要的东西。

纯数学面临同样的风险。「数学 1.0」要求证明可理解，因为只有人类的理解才能产出证明。结果是一个自我强化的循环：理解产生证明，证明产生更多理解，进而扩展了应用数学和科学可用的工具。生成经过验证却不可理解的证明的 AI 切断了这个循环。其下游后果 —— 对物理、工程、应用数学 —— 要数年才会显现。

这个论点直接适用于把数学基准表现当作训练信号的 AI 实验室。被优化成生成能通过 Lean 验证的证明、而不是能阐明机制的证明的系统，可能在基准上表现很好，却系统性地生产出「数学 2.0」正要防止的那种不透明、不可用的知识。《莱顿宣言》是一份关于数学中 AI 的社群治理声明，陶哲轩等研究者于 2026 年 6 月签署，开始围绕署名和质量评估建立规范，以保持这个循环完整。

「数学 2.0」真正需要什么

陶哲轩在结尾颠倒了标准的技术约束叙事。他说，「数学 2.0」最大的障碍不是算力、模型质量，甚至不是机构惯性。而是人类的想象力。

一个世纪以来，证明稀缺塑造了数学中的每一种激励结构 —— 评估指标、声望层级、资助标准、奖项竞赛的设计。重新校准其中任何一项，都需要想象不同的目标、一套描述进展的不同词汇，以及不同的人机协作结构。这些都不是技术问题。

ETP 和 IGP24 证明了「数学 2.0」的规范能支撑真正规模的研究。Mathathon 将检验它们能否在下一代数学家被「数学 1.0」的直觉完全塑造之前触及他们。即将到来的开源数学推理模型是强化证明稀缺的习惯还是打破它们，将取决于研究者带着怎样的框架来使用这些工具。陶哲轩的讲座是对那个框架的一份贡献：不是预言 AI 将征服数学，而是论证使用方式决定了下一代产出的数学最终是否有用。