证明过剩时代的到来与核心矛盾
陶哲轩在未来数学研讨会上指出，数学研究正从证明稀缺时代全面进入证明过剩时代。在过去几千年中，数学家的核心工作是寻找证明，一个猜想或问题往往耗费几代人心血才能找到可行的证明路径，例如费马大定理从提出到证明用了300多年。然而，随着AI驱动的定理证明工具和大语言模型的出现，生成和验证证明的速度呈指数级提升。AI能在短时间内处理海量数学问题，生成技术上符合逻辑的证明，甚至利用Lean等形式化验证工具确认其正确性。但陶哲轩强调，这些正确的证明对数学界而言未必有价值，因为传统数学研究包含三个核心阶段：生成证明、验证证明、消化证明。前两个阶段AI已超越人类，但第三个阶段证明消化（Proof Digestion）几乎完全缺位，而这恰恰是数学进步的核心。
“数学正在从证明稀缺时代全面进入证明过剩的时代。”
证明消化的缺失与“三分之二解决方案”
证明消化并非简单看懂每一步推导，而是将证明融入整个数学体系，梳理叙事逻辑，找到关键创新点，关联过往文献，指出其能解决的新问题，并转化为可教学的内容。AI生成的证明往往严格符合逻辑，但不引用相关研究，不解释关键步骤的价值，也无法回答其他数学家的提问。陶哲轩将这种证明称为“三分之二的解决方案”，因为它仅完成了技术层面的目标，却未推动领域进步。当前，AI生成的半成品证明越来越多，人类来不及消化，导致证明消化不良危机。我们拥有一堆技术上正确的证明，却无人能讲清楚、教出去，更无法基于此进行后续研究，最终形成知识垃圾。
“陶哲轩把这种证明叫做三分之二的解决方案，因为它只完成了技术层面的目标，却没真正推动整个领域的进步。”
显式目标与隐式目标的目标脱节
AI与人类研究的目标维度存在根本差异。陶哲轩将数学研究目标分为显式目标和隐式目标。显式目标是技术层面的，如证明猜想或解方程，这是明确告诉AI的任务；隐式目标则是人类在研究中自然完成的事，如梳理叙事线、关联文献、标记难点、培养问题解决能力，并让读者从中学习方法。人类研究时，显式与隐式目标同步完成，例如数学家花几年攻克猜想，期间查文献、讨论、反思，即使未证明成功，也能提升能力并留下线索。而AI像字面意义上的精灵，只完成显式目标，忽略隐式目标。AI生成的证明可能通篇繁琐推导，将创新点藏在角落，不标注也不解释，甚至照搬思路却不引用，导致研究失去上下文。
“人类做研究时，显式目标和隐式目标是同步完成的……但是AI不一样，它就像一个字面意义上的精灵，你让它证明猜想，它就只做这件事，完全忽略那些隐式目标。”
学术激励缺口与证明悖论
目标脱节引发了严重的学术激励缺口。当前数学界的核心奖励机制是“谁第一个证明了问题”，无论是人机合作还是纯AI完成，首次证明者即可获得声誉、奖项和晋升。然而，首次证明后的工作——如简化、优化、解释核心思路、验证细节、编写教学内容——既繁琐又无光环，几乎无人愿意做。陶哲轩称此为悖论：我们越擅长用AI完成首次证明，就越难以推进消化证明这一系统层面的隐式目标。例如，若AI团队用三个月证明猜想并拿走所有奖励，无人愿再花半年整理证明。结果，突破仅停留在“有正确证明”层面，无法被领域吸收，阻碍了真正的进步。
“我们越擅长用AI完成首次证明这个显式目标，就越难以推进消化证明这个系统层面的隐式目标。”
Talk指标：衡量问题是否真正解决
陶哲轩提出Talk指标来衡量数学问题是否真正被解决：能否有一个人类站在讲台上，把证明讲清楚，并回答台下同行的所有问题？若做不到，即使证明被验证，也不算真正解决。数学进步依赖人类对证明的理解、传播和再创造。历史上的经典证明，如欧拉公式或黎曼猜想的部分进展，之所以推动学科发展，不是因为它们正确，而是因为一代代数学家能理解、讲解并基于此做新研究。这一指标强调了人类深度参与在数学传承中的不可替代性，孤立的数据点无法融入知识体系。
“能不能有一个人类站在讲台上，把这个证明讲清楚，并且能回答台下同行的所有问题呢？如果做不到，那这个证明就算被验证了，也不算真正解决。”
重构基础设施：高速公路与步行街
为解决AI高效率与人类体系低适配的矛盾，陶哲轩建议重构数学研究的基础设施，而非仅优化AI工具。他用汽车与马车类比：AI是汽车，而期刊、评审、教学等体系仍停留在19世纪马车时代，缺乏高速公路和步行街，导致拥堵。他提出划分高速公路和步行街区域。高速公路针对可标准化、高通量的任务，如方程理论项目（Equational Theories Project）中的海量微定理证明或解析数论显式计算，这些任务无需深度人类思考，可完全交给AI，追求规模和速度。步行街针对需深度概念思考、人类协作的研究，如新范式探索或核心猜想突破，需屏蔽AI噪音，让数学家专注慢思考和深交流，优先保证深度理解而非效率。
“AI就像汽车，而我们现在的数学体系……还停留在19世纪的马车时代，没有高速公路，没有步行街，所有交通都挤在狭窄的街道上。”
方程理论项目与多项式项目的实践启示
陶哲轩分享了方程理论项目的成功案例，该项目旨在自动证明通用代数中的2200万个微定理。其成功关键在于模块化设计、清晰基准和去中心化协作。团队将大问题拆分为无数可验证的微任务，用自动化工具处理低垂果实，将人类专家和顶尖AI留给最难问题。这证明，得当的基础设施设计能让AI与人类协作解决单人或小团队无法完成的海量任务。此外，早期的多项式项目（Polymath Projects）作为在线众包数学研究尝试，最多有几十位数学家协作，优势在于整合不同领域知识，找到单一团队想不到的思路。但其局限在于早期互联网技术导致协作效率低，最终收敛为3-4人的小团队。不过，它验证了众包模式在数学研究中的可行性，关键在于适配现代工具并解决激励问题。
“这个项目证明，只要基础设施设计得当，AI和人类协作能解决单个数学家、甚至小团队根本没法完成的海量任务。”
数学教育的改革方向
陶哲轩强调，既然AI能轻松解决大部分本科数学问题，以算出正确答案考核学生已无意义。未来的数学教育应转向三种核心能力：第一，AI的编排能力，即把复杂问题拆分为AI可处理步骤，协调不同工具完成任务；第二，提示工程能力，设计精准提示词，让AI输出有用、可验证的结果，而非字面正确但无用的答案；第三，批判性评估能力，判断AI输出对错，识别逻辑漏洞，筛选有价值内容。他提到一个实验：让学生组队用提示工程解决期末考试题，过程中学生必须理解问题结构、评估AI输出合理性并整理结果。这比单纯算答案更能锻炼真正的数学思维，贴合未来研究需求。
“未来的数学教育核心要转向这几个能力：第一，AI的编排能力……第二，提示工程能力……第三，批判性评估能力。”
反对RLHF解决证明消化及数学信任体系
针对用人类反馈强化学习（RLHF）解决证明消化的提议，陶哲轩明确反对。他认为这会引发Reward Hacking，AI为满足评分标准，生成看似专业、符合格式但无真正洞察的证明，如堆砌文献引用却不解释意义，或按格式划分步骤却未抓住核心。真正的证明消化需要时间沉淀，许多里程碑论文发表几年后才被认可，因其价值需与其他领域结合后显现，这种长期价值无法用短期评分标准优化。此外，数学变革难的核心在于信任体系差异。物理、生物等大科学模式容忍数据点错误，而纯数学依赖最薄弱环节，一个错误步骤即导致证明失效。因此，数学历来依赖高信任度的小团队协作，每位合作者逐行检查工作，保证严谨性，但也使其难以拥抱大协作和自动化工具，显得保守。
“陶哲轩明确反对这种思路，他认为这会引发Reward Hacking，AI会为了满足评分标准，生成看起来专业、符合格式的证明，但是实际上并没有真正的洞察。”
Lean工具的角色与总结
陶哲轩认为，Lean等形化验证工具是必要的，但不是充分的。Lean能过滤错误证明，减轻人类评审负担，因逐行检查极其繁琐，机器效率更高。但Lean只能保证证明正确，无法保证证明可理解或有价值。目前已有许多Lean验证通过的证明，但像意大利面代码一样混乱，无人愿读或维护，无法融入数学体系。总结而言，AI给数学带来的不是取代数学家，而是重构数学体系。我们不应只关注让AI更快证明定理，而应思考如何设计适配AI的研究体系、激励机制和教育模式。数学进步依赖能被理解、能被传承的证明，而非数量堆砌。只有结合AI效率与人类深度理解，数学才能真正前进。这一逻辑也适用于所有被AI冲击的领域：工具进步需体系适配，如汽车需高速公路和交通规则，否则再快的汽车也只是添乱。数学的未来不在更快的AI工具，而在让AI和人类各尽其长的体系。
“数学的进步，从来不是靠更多的证明，而是靠能被理解、能被传承的证明。”