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