陶哲轩ICM警示：AI泛滥引发“证明消化不良”，数学界面临新危机
当全球还在争论AI解题能力时，最顶尖的数学家之一站上讲台，给出了一个令人不安的答案：能，而且强得惊人，强到可能引发灾难。
2026年7月底，费城，国际数学家大会（ICM），数学界的“奥林匹克”。菲尔兹奖得主陶哲轩登台演讲，题目仅六个单词：Mathematics in the Age of AI。他向顶级数学家们宣告：答案将多到令人应接不暇。
▲ 幻灯片核心：红色标注的“proof indigestion”（证明消化不良），标志着从“证明稀缺”向“证明泛滥”的范式转变
陶哲轩没有空谈，他展示了一组实测数据
名为First Proof的项目在2026年5月28日完成了一项测试：将10道高难研究题交给四套顶尖AI。专家从准确性与表述打分。结果，至少7道达到可发表水准。单题成本仅10至1000美元。
你没看错，过去需数月甚至数年攻克的问题，AI仅需几十美元、几小时即可产出期刊级解答。
基于此，陶哲轩提出一个“工作假说”供听众参考：
▲ 陶哲轩的“工作假说”：他不纠结AI“能不能”，直接探讨“能了之后怎么办”
他故意模糊“合理”的定义，聚焦于：一旦AI足够强大，整个系统将如何崩溃。
这是演讲中反复被引用的一页，陶哲轩绘制了证明的生命周期，并标记了各个堵点：
第一堵：AI生成的候选证明堆积如山。第二堵：验证通过的证明缺乏人类可读性。第三堵：优质稿件过多，传统同行评议不堪重负。第四堵：发表后的证明持续膨胀，社区来不及将其提炼为教科书定论。
他给这种系统性阻塞起名：proof indigestion，即“证明消化不良”。
直观类比：社会从饥荒直接跳到自助餐时代。食物充足，但厨师、检验员、营养员未变。食材满仓却无人处理。陶哲轩的比喻更精准：生成如觅食，验证如检验，消化（理解、讲解、转化为知识）如烹饪摆盘。我们将进入一个生食满冰箱、却无人烹饪的时代。
▲ 认知科学家Gary Marcus在X上称讲座“必读”，并总结了“证明消化不良”与“数学非均质”两点
陶哲轩将证明成熟度分为五阶段：生成、验证、阐释、发表、经典化。类比生命成长，“成年”阶段的教科书式证明才有应用价值，初生婴儿远不够格。
尖锐现象：有人用AI生成并验证证明后即“弃养”，仅留形式证书，无报告或评议。证明虽对，却是“孤儿”，难以辅助学习，其意义也无法判断。
反常现象：生成冗长正确证明比简短更容易。陶引用帕斯卡：“信写长因没时间写短。”AI证明动辄几十页、逻辑臃肿、层次混乱，虽步步正确，但让审阅者崩溃。
他在参与的项目中看到：自动形式化几小时完成数周工作，但冗余代码拖慢构建，人工审阅反更痛苦。
陶回顾优先权变迁：期刊发表日（曾现审稿人“抢跑”）；arXiv时间戳（解决旧题，引发“疯狂预印本”竞赛）；如今连arXiv嫌慢，有人直接在社交媒体抢先宣布。
当“首个解出”仍是声望货币时，大家拼命生成、抢着宣布，无人愿做“讲解、简化、综述”的工作，因那不酷、不算“第一”。
陶的提案：若竞争优先权，应授予能清晰报告并回答问题者；仅丢形式证书上网不应获此荣誉。
▲ 陶哲轩建议之一：规范披露AI协助，避免“暗用隐瞒”的恶果
同样呼吁见于集体文件。2026年6月，《莱顿宣言：人工智能与数学》发布，获IMU背书，内容如下：
▲ Leiden宣言对数学家的建议清单，含披露、审稿及开放科学
陶在ICM幻灯片中将Leiden宣言列为“从诊断到行动”的入口之一。这场消化不良已成学科系统性疾病。
X评论者迅速将“证明消化不良”推广至各行业。
▲ “解题与创理是不同能力。前者优化框架，后者发明框架。”
试想：文案、代码、法律意见、假说，一旦生成成本为零，瓶颈便移至审核、选择、整合与问责。数学因形式化验证可机器查“对错”；但“值不值得成理”“如何教学”“有何启发”等价值判断，算法无法自动完成。
陶用词精准：Goodhart定律。指标过度优化即失效。若学科只盯“解题量”“抢先宣布”等量化指标，如公司只看GMV不看利润，原本对齐的目标（解题、建理、育人、建设共同体）将被撕裂。
▲ 幻灯片“目标网络”：知识居中，连接解题、建理、育人、审美等，AI过度优化恐致分叉
陶自比历史：1900-1930年代危机（罗素悖论、哥德尔不完备），虽痛苦但产出更清晰公理与逻辑。他倾向乐观，但前提是共同体需主动适应，不能任旧体系溃败。
他还提醒：半世纪前解微分方程，六百年前算正弦表，如今计算机秒级完成，数学未终结，而是转型。本轮区别：生成速度与商业激励空前，可能在“新规则未建”时，旧声望与发表体系已被扭曲。
▲ 社交网ICM讲座幻灯片分享帖
数学，人类智识皇冠上的宝石，正经历消化系统重构。AI越强，积压越快。机器算出结果后，仍需人去读、去验证，并将其转化为人类知识体系中的活的一部分。
此问题不只属数学家，亦属即将被AI生成物淹没的行业，即属于我们所有人。