陶哲轩谈 Math 2.0 数学研究进入证明过剩时代
陶哲轩在 Caltech 的演讲里给数学的下一站起了名字，Math 2.0。过去近百年，数学运行在一套默认前提上：证明稀缺。找到一个开放问题的答案并证明它正确，既难又罕见。院系的传统、激励和考核目标都围绕这个前提搭起来。
AI 打破了这个前提。数学恰好具备机器学习最爱的三件东西：证明可被客观验证、可以数字化、还有海量高质量语料。数学家对哪些方向有意思会吵起来，但对什么算完整正确的证明有共识，Lean 这类证明助手甚至能机械校验。前沿实验室因此把数学解题能力排在优先位置。结果是，证明过剩的时代来了。
陶哲轩紧接着泼了盆冷水。AI 的能力极不均匀，在有些方向上惊人，在另一些方向上完全不够用。更麻烦的是展示环节，社交媒体上刷到的都是 AI 解出的题，失败尝试和沉默没人转发。他呼吁更透明的能力评估，要报告资源消耗和负面结果，First Proof 就是朝这个方向的一次尝试。
他的警告落在更深一层。解题只是数学的一个代理指标，在证明稀缺年代它大体靠谱，到了证明过剩年代就开始跑偏。开放问题像灯塔，不是终点，照亮的是那些还没走的路；AI 提前点亮灯塔，反而可能让周边地带失去探索价值。他还设了个思想实验，AI 拿出一个能通过三期临床的治癌配方，附上 Lean 证明，却没人理解其中机理，你敢不敢注射。
Math 2.0 的出路不是解题更快，而是让 AI 加固人类理解与数学之间的每条连接：解释证明晦涩的结果，把散落论文编成活的网络，做消融实验，探索定理邻域，训练可解释的数学专用模型。陶哲轩说，最大的瓶颈不是技术，也不是学术文化，是想象力。