夜雨聆风
数学家苦等一个证明的年代，可能正撞上一种荒诞的新麻烦：证明来得太多、太快，专家根本读不完。
2026 年 7 月 24 日，菲尔兹奖得主陶哲轩站上国际数学家大会（ICM）的公开讲台。他给这场潜在危机起了一个很有肠胃镜画面感的名字：proof indigestion，中文可译作“证明消化不良”。
AI 会做数学题，听起来像捷报陶哲轩关心的却是捷报塞满邮箱之后，谁来确认它、解释它，又由谁判断它配不配进入教科书。
一场以“假如”为开头的警告
先划清边界陶哲轩没有宣布 AI 已经接管数学他设置了一个 Working Hypothesis（工作假说）：在合理不久的将来，AI 工具可以用合理的成本、监督与成功率，完成相当比例的研究级数学任务。听众无需相信这个假说，只需暂时接受它，再观察制度会发生什么。
这层限定界定了他的论述范围社交平台把演讲浓缩成惊悚警告，原演讲的用意是测试数学制度在假设下承受的压力。Gary Marcus 转发时抓住两个重点：数学的工作并不同质，AI 也许擅长其中若干环节；每份证明的价值也有差异
▲ Gary Marcus 的转发帖附上“证明消化不良”与数学目标分叉两张幻灯片；帖子属于二手解读，核心论据来自陶哲轩原始幻灯片。
压力并非凭空想象陶哲轩展示了独立项目 First Proof（首证项目） 的第二批测评：2026 年 5 月 28 日，四种 AI harness（智能体编排系统）挑战 10 道未公开的研究级新题。专家同时审查正确性与 exposition（阐释质量），10 题中有 7 题至少有一队达到可发表水平，算力成本约为每题 10 至 1000 美元。
这组结果没有替 AI 颁发“数学家证书”。它透露出更实际的变化：研究级证明已经进入可重复测评，价格也低到足以批量运行。证明工厂的机器，开始转了
▲ 幻灯片列出第二批 First Proof 的受控条件、专家评审、7/10 成绩与单题成本。
证明写完，数学才刚走到第二站
普通读者容易把数学论文想成一道大题：答案正确，任务结束。陶哲轩在幻灯片里把真实过程拉成一条长链。开放问题先得到候选证明，随后接受核验；通过后还要写成同行能读懂的文本，进入发表与共同体讨论，最终被压缩进该领域的 definitive theory（定论性理论）。
▲ 陶哲轩拆出的六个环节：生成、核验、阐释、发表、消化与典范化。
Lean 等证明助手能逐步检查形式逻辑，像一台极其严厉的编译器。然而“机器验过”只解决了正确性的一部分。一个几百页的形式证明可能毫无逻辑漏洞，领域里的研究者仍要找出关键想法，辨认它与旧理论的关系，并把它教给下一代。
软件工程已经尝过类似滋味：代码生成按分钟计费，代码评审仍按人的注意力计费。数学更麻烦程序跑通就能交付功能，定理还要长成共同体可反复使用的知识。这里没有一键“加入教科书”按钮，多少有些不近人情。
从证明稀缺，突然冲进证明过剩
陶哲轩的核心幻灯片列出了后果：AI 证明会堆积等待核验；核验通过的结果会等待可读文本；传统同行评审会被大量正确且写得不错的证明压垮；发表之后，共同体依然来不及把它们整理成定论形式。
“In short, we will transition from an era of proof scarcity to an era of proof abundance.”
“简言之，我们将从证明稀缺的时代，进入证明过剩的时代。”
▲ 红字标出 impedance mismatches（阻抗失配）与 proof indigestion（证明消化不良）。
现实已经递来一张小票Erdős problems 公共题库近年成了 AI 数学试验场，高质量突破确实出现过；另一端也冒出了 100 至 200 页的 AI 长文。题库维护者 Thomas Bloom 观察到，有人让 AI 生成、检查并写完论文，没有人从头读过，之后也不会有人去读。
于是，形式正确与数学进步之间露出一道缝。若“首证数量”成为唯一排行榜，Goodhart 定律很快生效：一个指标一旦被当成目标猛冲，它便开始失真。容易自动化的题会吸走资源，专家时间则耗在清理结果、追查旧文献和识别漂亮幻觉上。
证明变便宜之后，理解成了奢侈品
陶哲轩给出的药方颇朴素他支持把《莱顿人工智能与数学宣言》作为起点，要求研究者披露 AI 工具使用，并主动降低同行核验成本。他还提出一个 talk-test（报告测试）：作者若无法清晰、正确、以专家水准讲解成果，并妥善标明贡献来源，结果就不该发表。
▲ 莱顿宣言给个人数学家的建议：披露工具使用、支持审阅需要，并由人类作者继续承担正确性责任。
这条门槛把责任重新落到“理解”上未来最稀缺的数学劳动，可能集中在挑选值得追的问题、把冗长论证压成清楚概念，以及维护一套后来者能够信任的知识体系。机器可以制造更多候选答案，人类共同体还得决定哪些答案值得留下。
AI 数学最让人忧心的时刻，或许会出现在它答题太快之后。 那时，数学家面对的难题将变成一座不断增高的证明仓库。门口贴着一行很冷静的告示：正确，仍待理解。
