陶哲轩 Caltech 演讲「Math 2.0」：AI 让证明不再稀缺，只盯着解题已经开始伤害数学

这件事意味着什么

【要点】

陶哲轩 10 月 9 日晚（美西时间）在加州理工做了公开演讲「Math 2.0」，第二天把 27 页讲稿传到个人博客。他说这场演讲一年前就定了，原题是「机器辅助证明」，因为最近的事改动很大。

核心判断有三条。第一，数学过去一百年建立在「证明稀缺」上；证明能被客观核验、完全数字化、语料又多，所以前沿实验室优先猛攻数学，「我们正在进入证明过剩的时代」。第二，社交媒体上看到的都是 AI 解出的题，但前沿上的大多数问题即使砸下大量算力依然没解出来，失败的尝试很少被报告；他呼吁评估 AI 能力时完整报告资源消耗和负面结果。第三，解题本来只是更长远目标的代理指标，证明稀缺时还算准，现在已经失准，「继续盲目优化解题，正在实际伤害数学的长期健康」。

他给出的替代用法包括：给证明晦涩的已知结果找讲得通的解释、把大量论文串成可实时更新的结果网络、扩充 Mathlib 形式化库，以及开发可解释的开源数学模型，并预告「一些开源数学模型很快就会发布」。

【可核验】

博客原文与讲稿 PDF 见本条链接（讲稿：teorth.github.io/tao-web/slides/math-2-0-caltech-2026.pdf）。讨论最多的是一页思想实验：AI 找到一种抗癌药物组合，模型预测已在 Lean 里核验、也通过了三期临床，打进身体前你是否希望至少有一位人类专家理解它的机理。Andrew Curran 引用这页反驳「晚期癌症病人根本不在乎」，约 121 万浏览、579 次引用；X 上相关讨论 24 小时约 280 帖，最近几小时每小时 17 到 27 帖，仍在升温。

【我们的判断】

这场演讲比 AHM 那份抵制声明更值得认真对待，因为它提的要求实验室做得到。本周两份 AI 数学成果正好是样本：DeepMind 在《科学》上写明 353 道 Erdős 问题解出 9 道，OpenAI 说约 4000 道题筛出 722 篇、每题约 3 小时 Pro 算力，分母和算力都给了，缺的是失败尝试的细节。谁先把失败和成本也公开，谁的「解出了」才有分量。

癌症那页被批评者读窄了。它的要害不是「人要看懂才算数」，而是 Lean 只能保证证明符合形式化后的命题，保证不了命题本身对应真实世界；试验设计有漏洞，被 AI 找到并利用，机器核验照样全部通过。人类理解在这里是审计层，不是情怀。我们接下来盯两件事：他预告的开源数学模型由谁发布、能否复核；实验室下一轮数学发布会不会开始附上失败率。