夜雨聆风数学家们终于开始担心：问题恰恰在于AI太能写。
2026年7月24日，费城，国际数学家大会（ICM）主会场。台下坐着上千位来自全球的顶尖数学家。台上，菲尔兹奖得主、当今数学界最耀眼的名字，陶哲轩，讲出了一个令满场静默的判断：
他的判断可以概括为：AI未必会终结数学，却可能把数学活活“撑死”。
他给这种病起了个名字，叫"证明消化不良"（proof indigestion）。
▲ ICM 2026现场投影页，展示陶哲轩关于"proof indigestion"的警告
证明“堆成山”，没人啃得动
故事要从一个反直觉的事实讲起
过去几百年，数学的稀缺资源一直是证明本身，找到一个定理的证明，是整条价值链中最贵、最难、最受尊敬的环节。谁证出来，谁拿奖，谁载入史册整个学术系统都围绕"谁第一个交卷"而建。
但2025年到2026年之间，事情起了质变。大语言模型配合形式化证明助手（如Lean），开始以工业级速度喷涌出数学证明草稿。陶哲轩在讲座中引用了一组数据：2026年5月的"First Proof"盲测挑战中，四个AI系统对十道研究级新题开考，七道被至少一个团队解到了"可发表质量"，单题算力成本不过10到1000美元。
十美元一道研究级数学题
这个数字像一记闷拳它意味着，证明的"出厂价"正在跌向零
▲ 陶哲轩ICM讲义核心页：从"证明稀缺"到"证明丰裕"，中间是四层积压
但跌价的只是生成在陶哲轩的框架里，一道数学问题的完整解决要过三关：
- 证明生成
，找到一套论证。AI已经很能干了。 - 证明验证
，确认论证没有逻辑漏洞。形式化工具可以"编译通过"，给出极高确信度。AI正在快速接管。 - 证明消化
，理解它到底意味着什么。主线是什么？跟旧理论怎么接？能不能教给研究生？能不能启发下一个问题？能不能写进教材？
前两步可以自动化第三步，截至目前，只能靠人
于是灾难场景就出现了：AI以每天几十篇的速度生成逻辑上正确的证明，堆在数学共同体的"仓库门口"。验证或许也过了，但理解、阐述以及纳入知识体系的工作都无人完成。
这就是proof indigestion：证明多到共同体消化不了，仿佛被撑住。
生肉丢上餐桌，不算一顿饭
陶哲轩在Mathstodon上写过一个绝妙的比喻。
他说，把数学研究想象成做饭证明生成是觅食采集，验证是清洗检疫，消化是烹饪上桌。在食物稀缺的年代，谁能带回猎物谁就是英雄，没人挑剔你的摆盘。但当食物过剩了呢？
你不会欢迎一个陌生人，把一块来路不明的生肉扔在聚餐桌上，说"搞定了"。
这个比喻精准到刺痛它直指一个正在数学界真实发生的场景：有人用AI跑出一个证明，往arXiv一扔，宣布"问题已解"，然后就走了。 这类提交缺少阐述、文献梳理、同行评议和可读的写作。甚至提交者自己都承认，"我也没完全看懂"。
陶哲轩把这种行为比作遗弃他说，作者应该是证明的"监护人"，有义务把它养到至少"成年"，能被讲解、能被发表、能被审阅。只生不养，把"养育"甩给社区，是他明确批评的做法。
他甚至提出了一个激进的打分法：仅提出未验证的证明，最多算"三分之一解"。生成且验证，只算"三分之二"只有经过妥善消化，才算完整的解
一个反直觉的标签：问题已解，但仍然"开放"
现实中已经出现这样的案例陶哲轩自己维护的Erdős问题站点，已经变成了消化不良的活体标本。
Erdős问题是数学界的"悬赏任务清单"，源自传奇数学家保罗·Erdős几十年间随手提出的成百上千个公开问题。陶哲轩的站点一直在追踪这些问题的进展。而在GPT-5.5发布之后，声称已解的提交一度积压了近二十个，此前这个队列通常只有一两个。
站点甚至不得不发明一个新标签："open (Lean)"。
意思是：这道题在Lean形式化证明助手里已经有可检验的完整证明了，编译器说它是对的，但在人类理解的意义上，这道题仍然算开放。
逻辑上正确、形式上可验证、却无人理解的证明，这在数学史上几乎是新物种。它让人想起1976年的四色定理：Appel和Haken用计算机穷举上千种情形，证明了任何地图只需四种颜色，但当时数学界争论了很久，"人读不动的正确证明"，到底算不算证明？
五十年后，同样的哲学困境回来了如今，它已经从一道题的孤例变成每天都在发生的量产事件。
能力之争之后，还有价值之争
▲ 讲义中的数学目标网络：过度优化任何单一目标，都可能让其他目标"撕裂"
陶哲轩在ICM讲义中做了一件非常聪明的事。他避开了"AI到底能不能做数学"的口水仗，让听众先接受一个"工作假设"，假设AI已经足够强了，随后抛出另一个问题：
我们到底在优化什么？
数学有很多目标：解题、建理论、理解世界、培养下一代、创造审美价值、服务应用。过去，这些目标大体正相关，你解了难题，通常也推进了理论、训练了学生、产出了美。但AI和商业激励正在把这些目标拆散。
这就是经典的古德哈特定律：当一个指标变成目标，它就不再是好指标。 如果数学界把"解了多少公开问题"当作核心KPI，AI可以帮你把数字刷得极其好看，代价是理论建构停滞、教育空心化、审美退化。
陶哲轩的建议是：降低对"证明生成"和"抢第一"的权重，提高对阐述、消化和经典化的权重。 评价重点应转向谁能最先清晰地公开讲解，而非谁最快提示模型。
每个行业都在被"撑死"
这个判断击穿了数学的围墙
▲ 评论区一针见血："消化不良即将冲击每个行业。生成变便宜了，验证没有。"
有人在评论区写道："Proof indigestion is about to hit every industry, not just math. Generation got cheap. Verification didn't. Someone still has to read the stuff."
生成变便宜了验证成本没有下降总有人得读那些东西
这句话像一把钥匙，打开了AI时代一个被严重低估的结构性矛盾。代码可以自动生成，但code review的人没有变多。论文可以批量产出，但审稿人已经不够用了。开源社区被AI生成的低质量Pull Request淹没，维护者不堪重负。到处都是"食材"，到处都缺"厨师"
早在2017年，Distill上就有一篇经典文章叫《Research Debt》，研究债务。作者Chris Olah把学科进步比作登山：后来者攀登的是前人几百年堆起的山，而山高不等于路径合理。糟糕的阐述、未消化的想法、拙劣的抽象，共同构成了天文数字的认知债务。
▲ 2017年Distill的经典文章《Research Debt》，被认为是"证明消化不良"的跨领域前传
▲ 有人直接指出：陶哲轩的"证明消化"和Distill的"研究债务"说的是同一件事
九年之后，陶哲轩在数学领域精确复现了同一个诊断。而AI，正在把债务的生产速度提高到人类可能永远还不清的程度。
直升机登顶，但脚下没有路
陶哲轩对《大西洋月刊》说过一个意味深长的比喻。
他说，难题像远方的营地过去数学家徒步过去，路上留下路标、地图、小径，供后人使用。AI像直升机，能直接空降到终点你到了但你失去了旅程的全部副产品
这番话指向知识本身的形成路标和地图就是数学知识的核心定理的价值不仅在于它是"真的"，更在于证明的过程揭示了结构、联系和直觉，正是这些东西训练了下一代数学家的"解题肌肉"。
他在教育场合用过另一个更扎心的类比：食物从稀缺到丰裕之后，危机从饥荒变成肥胖和体能退化。认知摩擦被AI抹平之后，风险是学生的思维肌肉开始萎缩，成绩上升、能力空洞、耐心消退、对真实批评的耐受力下降。
AI可能成为认知领域的垃圾食品，好吃、便宜，让你再也不想自己做饭。
一场新的"基础危机"
陶哲轩在讲义中把今天发生的事情，类比为二十世纪初的数学基础危机，罗素悖论、哥德尔不完全性定理，那些动摇了整个学科地基的风暴。
但他说，这次危机的对象转向了数学实践的基础：什么算成功？什么应被奖励？共同体到底在优化什么？
他欢迎这场动荡他甚至期待数学中出现更多"人文学科式"的争论，关于什么才算好的数学，关于写作、洞见与审美在评价体系中应该占多大权重。证明稀缺的时代可以容忍"正确但写得烂"；证明丰裕的时代，该提提品位了
就像食物丰裕催生了美食文化，证明丰裕或许也能催生，如果我们足够清醒的话，一种更讲究"理解"的数学文化。
这是一个菲尔兹奖得主，在四年一度的数学界最高殿堂上，对全世界同行说出的最温柔、也最残忍的提醒：
AI能帮人证明定理；若无人能把它讲明白，这些证明对人类便失去意义。
