Math 2.0来了
昨天陶哲轩（Terence Tao）在Caltech做了一个讲座，题为“Math 2.0”，相信大家对于近期AI在数学领域的众多突破有所了解。去年7月，DeepMind的AlphaProof和AlphaGeometry 2在IMO上拿到银牌水平，其中AlphaProof解决了最难的题目。到了今年，AlphaGeometry 2已经把过去25年IMO几何题的解决率提升到了84%。字节跳动的Seed Prover和Harmonic的Aristotle也在2025年IMO达到金牌水平，高中竞赛这个赛道基本上已经被AI攻破了。
那么大学和前沿研究层面，中科院团队开发的Numina-Lean-Agent成功形式化证明了2025年Putnam竞赛全部12道题，这是世界上最难的大学数学竞赛。今年4月，北大董彬团队用AI框架解决了交换代数中悬置十余年的Anderson猜想，并在Lean 4中完成了约19000行的形式化验证，效率比有经验的专家提升了至少10倍。5月，OpenAI的模型破解了困扰数学界80年的平面单位距离问题（埃尔德什猜想），剑桥大学的蒂姆·高尔斯评价这是“人工智能数学的一个里程碑”。
陶哲轩自己主导的First Proof项目第二期结果也值得关注。他们选了10道从未公开过解法的前沿研究级新题，用双盲同行评议的方式让AI作答，结果有7道达到了学术发表标准，成本最低只要8美元一题。其中一道随机偏微分方程的问题，AI甚至给出了跟人类完全不同的解法，推导出了更强的中间结论。
陶哲轩在PPT里提出了一个我认为是整场演讲最关键的判断：传统数学（Math 1.0）的整套制度（学术评价、经费申请、人才培养）都建立在“证明稀缺”这个假设之上。解决一个开放问题极其困难，需要极高的专业知识和大量时间。但现在，这个假设正在被打破。问题在于，当AI可以批量生产证明的时候，数学界需要重新思考一个根本问题：这个学科的核心目的到底是什么？
他用了一个很精准的比喻：开放问题就像“灯塔”，它们的价值不在于被“攻克”，而在于指引数学家去探索周围未知的领域。在尝试解决这些问题的过程中学到的东西，无论是成功、失败还是部分进展，往往比最终的解本身更有价值。但如果AI过早地、批量地把这些灯塔“点亮”，反而可能破坏周围探索的生态。
这引出了一个更深的忧虑。陶哲轩在PPT里用一个非常尖锐的思想实验来说明这个问题：假设你被诊断出早期癌症，AI推荐了一种由之前未知的化学物质组成的鸡尾酒疗法，它声称能杀死所有癌细胞，并且通过Lean形式化验证了其数学模型的正确性，甚至通过了三期临床试验。但在把这种液体注入你的血管之前，你是否会想知道：至少有一个人类癌症专家，能部分理解这个疗法背后的机制？
这个思想实验直指核心：可验证性不等于可理解性。AI生成的证明可能逻辑上完全正确，但如果人类无法理解它为什么正确，这种“正确”在应用层面就是脆弱的。
陶哲轩本人的态度转变很有代表性。他此前一直是结合AI与数学形式化的积极倡导者，但今年9月，他联合25位菲尔兹奖得主发布了《人工智能在数学中的严重错位》声明，批评AI企业将攻克数学难题作为大模型性能基准的做法对数学本身造成了损害。他牵头的“人类数学协会”也发表声明呼吁停止与OpenAI合作。这种态度转变的背后，是整个数学界正在经历的分裂。一方面，AI确实在帮助数学家做以前做不到的事情，比如中科院团队用Numina-Lean-Agent与人类专家协作，在两周内完成了对一篇论文的形式化证明。另一方面，AI批量产出的结果让很多数学家的研究节奏被彻底打乱。一位研究员在采访中说得很直接：“这些‘数学家’搞到一半的‘难题’没了，他们都没法结题，更不要说申请后面的经费了。”更麻烦的是验证工具本身也不是万无一失的。2026年夏季，Lean接连暴露出多个健全性漏洞（Soundness bugs），被圈内称为“健全性漏洞之夏”。如果连“终极裁判”都不可靠，AI生成的证明又该由谁来把关？
陶哲轩在PPT里给出的方向是：Math 2.0的核心任务不是继续优化解题，而是增强人类理解与数学之间的所有交互方式。他列举了几个具体的实践方向：
[*]一是“开放阐释问题”——找到那些已知证明难以理解的结果的更好的解释，而不是继续攻克新的问题。Caltech的Mathathon就是这个方向的实验。
[*]二是把大量研究论文整合成更大的“活网络”，比如Integrated Explicit Analytic Number Theory Network（IEANTN）【PPT Page 26】。
[*]三是建设大规模的形式化数学库，比如Mathlib【PPT Page 24】。
[*]四是用AI来发现和突出新的原理、方法或洞见，而不仅仅是新的证明【PPT Page 24】。
他还提到了“消融研究”（Ablation Studies），即拿一个已经证明的定理，看看移除某些关键理论或输入后，它是否还能被证明。比如为目前只能用非初等方法证明的结果找到初等证明【PPT Page 27】。陶哲轩最后说了一句话我印象很深：实现Math 2.0的主要瓶颈不是技术，甚至不是制度文化，而是想象力【PPT Page 28】。
欢迎大家一起讨论。尤其在数学或相关AI领域的一线研究者的看法。
（帖文中涉及的PPT内容引自Terence Tao, “Math 2.0,” Caltech, October 2026。https://teorth.github.io/tao-web/slides/math-2-0-caltech-2026.pdf）
{:5_106:}
页:
[1]