🧮 数学 2.0：陶哲轩提议给「解题」降级
一个职业的底层假设能稳定一百年，本身就罕见。数学研究算一个：找工作难、证明更难、发表证明难上加难，整套激励都建在同一个前提上——证明是稀缺品。今年 10 月，陶哲轩在加州理工学院的演讲《Math 2.0》把这个前提当众拆了。幻灯片 29 页，挂在他个人主页上，传到 Hacker News 当天三百多分。
🧮 数学 2.0：陶哲轩提议给「解题」降级
一个职业的底层假设能稳定一百年，本身就罕见。数学研究算一个：找工作难、证明更难、发表证明难上加难，整套激励都建在同一个前提上——证明是稀缺品。今年 10 月，陶哲轩在加州理工学院的演讲《Math 2.0》把这个前提当众拆了。幻灯片 29 页，挂在他个人主页上，传到 Hacker News 当天三百多分。
他的论证起点是三个性质。数学证明客观可验证，写成 Lean 这样的证明助手语言就能让机器判卷；证明高度可数字化，不需要任何真实世界的数据和实验；围绕证明积累的文献庞大且质量极高。可验证、可数字化、数据好——恰好是机器学习最擅长吞下的三样东西。前沿实验室把钱优先砸向了这里，于是数学率先撞进了一个新时代：证明过剩。
过剩到什么程度？幻灯片里给了两个已经发生的例子。等式理论项目（ETP）在 2024 到 2025 年众包人和机器一起，判定泛代数里两千两百万条命题的真伪——两千万条，人手一天判一千条也要六十年，机器加流程把它收进了两年的项目窗口。Inverse Galois Problem 挑战赛今年办了第一阶段：度为 24 的多项式对应两万五千种可能的伽罗瓦群，一场众包竞赛给每一种都找到了代表多项式，第二阶段要推进到度 31。
但陶哲轩给这场狂欢泼的第一盆水，是他引用的一条社交媒体错觉：「我刷到的数学题怎么全被 AI 解了！」原因是报告偏差——成功的解法发新闻稿，失败的和烧掉的算力没人写。他呼吁对 AI 能力做更透明的科学评估，把资源消耗和负结果一起报账，还点名了一个叫 First Proof 的尝试。能力本身也是锯齿状的：某些方向惊人，另一些方向无能，中间隔着一条不均匀的边界。
整场演讲最重的部分，是「灯塔」。
纯数学里的开放问题，作用像海岸线上的灯塔——它们从来不是目的地，是导航。船朝着灯塔开，真正的收获是沿途被照亮的那片海域：新工具、新联系、失败路上捡回来的引理。等哪天自动工具一秒把你传送到灯塔脚下，问题解决了。海域却没人看过。他的用词是「绝育」（sterilize）：那片数学景观从此没有新的人生长出来。这条警告对应着他画的一张生态图——旧循环里，纯数学证明产出的理解可以安全地输送给应用数学；新循环里，AI 绕过理解直接产出证明，其中一部分对齐、一部分错位，错位的那部分会顺着管道流向真实世界。
他画了一个思想实验。让一个高级 AI「找到能通过三期临床的癌症疗法，不许出错」，烧完算力，它端出一杯成分不明的鸡尾酒，居然附带一张 Lean 证书，居然真的通过了三期试验。现在轮到你被诊断出早期癌症，聊天机器人推荐你打这一针——打之前，你会不会希望世上至少有一个人，哪怕只理解这个疗法机制的一小部分？理解的值钱之处在这里显形：它是给对齐买的保险。
于是 Math 2.0 的清单几乎是反着开的：不比谁解题快，比谁把理解和数学的接口焊得更牢。做「开放讲解问题」——给那些证明过程晦涩的已知结果寻找更有动机的解释；把论文织成活的网络，比如他参与的分析数论活表格 IEANTN；养 Mathlib 这样的形式化数学库；用 AI 找原理和方法而不只是证明；甚至做定理的「消融实验」——把一个定理的关键假设删掉，看还能救回多少结论。他预告了一批开源、可解释的专用数学模型「很快发布」。连 Caltech 自家的 Mathathon 都改了章程——本站九月初记过它两次改期，这次幻灯片给出的日期是 11 月 13 日到 15 日，学生组队用开源 AI 工具给「现有证明不满意的结果」找更好的证明，比赛项目从解题换成了讲解。
演讲的最后一张幻灯片只有一句话，值得原样抄在这里：这件事的主要瓶颈，并非技术，甚至并非学界文化，而是想象力。
解题这一数学家的传统主业，被他亲手从目标降级成了指标——一个曾经在稀缺时代准确、如今已经失真的指标。下一个十年的数学家也许会这样回忆：我们曾经用「解出了什么」来衡量自己，后来学会了用「理解了什么」。