证明要过剩了：陶哲轩说数学的下一场危机是消化不良
Mathematics in the age of AI
2026 年 7 月 24 日，陶哲轩在国际数学家大会（ICM）做了一场面向公众的演讲，题目是《Mathematics in the age of AI》。开场他把当下类比成 20 世纪初那场数学基础危机——罗素悖论和哥德尔不完备定理逼着数学家把「什么是集合」「公理是什么」这类一直丢给哲学家的问题重新算清楚，动荡三十年换来一套至今可信的地基。他说我们正在进入一段类似的动荡期，只是这次要清算的不是逻辑基础，而是数学共同体的价值与实践的基础。
最值得学的是他怎么处理「AI 到底行不行」这个所有人都在吵的问题：他直接把它请出了场外。他把它写成一条「AI 能力猜想」——不久的将来，某些 AI 工具能以某种成本和某种程度的人类监督，完成某些领域的研究级数学任务——然后说，我今天不论证它，请各位假设一个足够强的版本成立。剩下整场演讲都是条件分析：如果这是真的，我们该改什么。把吵不出结果的事实判断和必须现在就做的价值判断切开，这个动作比他后面任何结论都通用。
唯一被他允许上场的证据
关于能力他只提了一组数据：First Proof 挑战（1stproof.org）。这是个独立评测项目，每批十道新的研究级问题，第二批在 2026 年 5 月 28 日按受控科学条件测了四套 AI harness（模型加上外围工具与流程的整套系统），由领域专家就正确性和表述质量分别评审——十道题里七道被至少一支队伍解到可发表质量，每题算力成本 10–1000 美元。他挑这组有讲究：他明说支持或反对能力猜想的数据点很多，但大多不在受控条件下收集，高度受报道偏差和非科学激励影响，关键成本和变量常常没披露。
古德哈特定律要把数学的目标撕开
数学研究一直有一堆并列的理由：解决未解问题、发展新理论、理解世界、培养下一代、留下有审美价值的作品。他的关键观察是：过去这些目标彼此正相关，推进一个通常也推进其他几个，于是可以拿一两个当其余的代理指标，剩下的不必明说。
而古德哈特定律（1975）说：当一个衡量指标变成目标，它就不再是个好指标。他认为生成式 AI 本身缺乏根基（ungrounded），加上 AI 公司的财务激励，让这条定律在这里格外容易生效。一旦过度优化某个指标，原本对齐的目标就会朝不同方向散开——刷奥赛题、刷 Erdős 问题，和建立理论、培养学生、写出能传下去的东西，会开始互相拉扯。
四次改写目标，问题全在后半段
他拿「解题」做案例，把目标当场改写了四次。第一版：尽可能多地解决未解问题。这个指标的后果早在 AI 之前就见过——一大批错误的黎曼猜想证明。第二版：加上「并验证其正确」。形式化验证（用 Lean、Rocq 这类证明助手把证明写成机器能逐步检查的代码）确实同时加速了生成和验证。接着是他最扎人的一问：如果 AI 产出一份长证明，没有任何人看懂——包括提示它的那个人——算什么？这不是假设：erdosproblems.com 上已堆了几十份 AI 生成的证明提交，很多大概是对的，但没有专家出来核验背书，有几份连提交者都声明没这个能力。
第三版：再加上「能被清楚地讲给同行」。AI 在这一环的记录很割裂——拼写、语法、格式近乎无可挑剔，但常常在琐碎处长篇大论，最有新意的部分几句带过，也不提和已有文献的关联。更微妙的是：人写的证明里，作者当年卡住的地方会留下天然的摩擦，读者到那里自然慢下来；被 AI 打磨得过分顺滑的证明抹平了这种摩擦，难点和例行推导读起来一样轻松。他引了 Thurston 1994 年的话：衡量成功的标准是我们做的事能不能让人把数学想得更清楚。
第四版直到终版，他把「被同行消化、接受，最终写进领域权威教科书」也加了进来，完整链条成型：生成证明 → 验证正确 → 写清楚 → 发表并被接受 → 正典化。他判断，如果能力猜想成立而政策和文化不变，链条会在后半段处处淤积：等验证的堆积，验证过的等人写成可读版本，正确又写得好的会淹没评审，发表出来的也多到无法整理成定论形式。他称之为从证明稀缺进入证明过剩的时代——部分症状在 AI 之前就已显现。他特意点出，正典化最慢、最依赖共同体共识、最不可能被 AI 优化，同时也最有价值：今天 AI 能在数学上做出成绩，恰恰建立在人类几百年攒出的那套权威理论之上。
三条他愿意给出的建议
一，把 AI 使用的负责披露变成常态——最坏情形是偷偷用又隐瞒以免被批评；他自己就在脚注写明幻灯片的文字补全和图表由 AI 参与生成。二，降低对「生成证明」和「第一个解出来」的重视，提高对「消化证明」（表述、发表、正典化）的重视；他点名 Leiden 宣言（leidendeclaration.ai）作为起点。三，一条经验法则：如果作者不能令人信服地就自己的结果做一场清楚、专家水准、正确且署名恰当的报告，这个结果就不该发表。
本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。 篇目由编辑独立选取，来源均经人工核实。