夜雨聆风证明太多，读懂的人太少 2026年夏天，全球最负盛名的在世数学家，站在国际数学家大会的讲台上，对着全世界同行说出了这番话。
7月24日，菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩（Terence Tao），在四年一届的国际数学家大会（ICM 2026）上发表公开讲座。52页幻灯片，标题只有六个词：Mathematics in the Age of AI，人工智能时代的数学。
他把焦点移到了一个棘手的问题：如果AI已经能大规模生产数学证明，而人类根本来不及看懂，那怎么办？
数学圈的新词：Proof Indigestion
陶哲轩造了一个隐喻，迅速成为整场风暴的中心词，Proof Indigestion，直译"证明消化不良"。
什么意思？过去几百年，数学界的瓶颈一直是"证明太少"。一道好问题，可能等几十年、上百年才等来一个正确的证明。找证明的人，往往也是最理解证明的人，因为你苦思冥想了那么久，写出来的时候你已经把每一步嚼烂了。
但AI改变了游戏规则
如今的前沿模型加上自动化框架，可以批量生成证明，再用Lean等形式化工具机器验证，也就是说，一台机器吐出一段推理，另一台机器检查它逻辑上没有漏洞。生成和验证都在加速，但人类的理解速度没有变。
于是出现了一个前所未有的局面：正确的证明堆积如山，却没有人有时间读懂、讲清楚、写进教科书。
陶哲轩在幻灯片上用红色标出这个词，并列出四重失配：AI生成的证明等着被验证；已验证的证明等着被写成人话；写好的证明淹没了同行评审系统；即使发表了，也多到社群无法消化成定论。
▲ 讲座核心页：红色标注的 impedance mismatches / proof indigestion，底部写着，从证明稀缺到证明丰裕
数学界告别了"吃不饱"，却可能"撑到吐"
两千美元，十道世界级难题
陶哲轩的警告并非杞人忧天就在讲座后的第八天，丰裕时代的象征性高潮如期而至。
8月1日，OpenAI研究员Noam Brown宣布：内部模型Astra解决了数学与理论计算机科学中的十项重大开放问题，涉及球面装填、编码界、非sofic群、Connes刚性猜想反例、Ramsey理论等。论证由系统生成，人类协助整理并在Lean中形式化。按API价格粗算，总成本大约两千美元。
▲ OpenAI研究员Noam Brown发帖：Astra内部版解决十项开放问题
两千美元一个数学教授可能花十年都啃不动的问题，机器用一笔咖啡钱的算力就"解决"了。
但"解决"这个词，恰恰是陶哲轩要我们重新审视的。
一个叫Pavel的用户随即在社交平台写下他的焦虑："我学数学远超一万小时，仍然无法轻易读懂这些证明。我读博士的朋友，如果不在那个子领域，也验证不了。" 他追问：世界上有足够多的聪明头脑去验证未来AI的产出吗？
▲ 用户Pavel的焦虑：学了一万小时数学，仍看不懂AI的十条证明
数学科普账号Musings on Math回复说：陶哲轩在ICM上正在谈这件事，数学界正被AI证明淹没，合格的评判者远远不够。
▲ 回复Pavel：陶哲轩在ICM 2026讲到了这个问题，甚至可能出现专家也无法理解的证明
生肉丢在桌上，谁来做饭？
陶哲轩用了一个绝妙的比喻
在食物稀缺的社会，猎人带回任何猎物都受尊敬。但在食物丰裕的社会，你不能闯进别人的聚餐，把一块生肉甩在桌上，然后让别人去清理、烹饪、上菜，那不叫"贡献晚餐"。
AI批量生成的"原始证明"就是这块生肉。正确，但生的 它仍需烹饪（阐述）、摆盘（写作）、上桌（同行评审）和品尝（社群消化），最后才可能变成食谱（进入教科书）。
他把整个"问题被解决"的过程拆成了一条六级流水线：
开放问题 → 未验证解 → 已验证解 → 写得好的解 → 被接受的解 → 定论性解
对应六个动作：生成、验证、阐述、发表、消化、经典化。AI正在猛踩前两步的油门，后四步的交通却还是牛车速度。
他甚至提出一条经验法则：如果一个结果的作者不能做一场清晰、专家级、正确归因的学术报告，那这个结果就不应该被视为已完成的发表。 因为你"生成"了它，不代表你"拥有"了它
▲ 讲座中的目标分化示意图：以"数学知识"为中心，箭头指向解题、建理论、培养后学、创造审美作品等多个方向，它们曾经同向，如今可能分叉
一场数学界的"基础危机"正在到来？
讲座开篇，陶哲轩回顾了一段大多数人已经遗忘的历史。
1900年到1930年间，罗素悖论、哥德尔不完备定理相继炸响，整个数学的地基都在摇晃，什么是集合？什么是数？无穷到底能不能用？那是数学史上著名的"基础危机"结果是动荡的三十年催生了更坚固的公理化框架。
陶哲轩说：我们可能正在进入一场类似的危机。 这场危机落在数学的价值与实践体系：什么算贡献？谁获得声望？论文的最低质量门槛在哪？一个证明是否必须是人类可讲授的？
幻灯片上，他引用了已故菲尔兹奖得主William Thurston 1994年的判断：衡量数学成功，应看它能否让人更清晰、更有效地思考数学，不能只数定义和定理的产量。
三十多年后，这句话被投射在国际数学家大会的屏幕上，对着一群正目睹AI产能飙升的数学家。讽刺与力量并存
解题≠创造，但问题远不止于此
AI评论者Gary Marcus迅速转发了讲座要点，并附上两张幻灯片截图。他提炼出两条：第一，证明的用处各不相同，存在proof indigestion风险；第二，数学并不均一，AI可能只擅长其中一部分。
▲ Gary Marcus称讲座"brilliant, must read"，并联系Astra评论：擅长某类解题，但尚无证据能构建新理论
帖子下面，一条回复精准得像一把手术刀，
"解证明和创造理论是根本不同的能力。一个在框架内优化，一个发明框架。"
▲ 一位用户的回复：Solving proofs and creating theories are fundamentally different capabilities.
这与陶哲轩在讲座中"理论构建需另案分析"的判断不谋而合。Erdős题、奥赛题、某些离散数学的上下界改进，这些可能落在模型的"搜索友好区"。但开辟全新的数学语言、定义新对象、提出新问题层级？那仍然可能是另一个维度的事
陶哲轩在早前接受《大西洋月刊》采访时也说过类似的话：很多AI攻克的问题属于"cheap wins，廉价胜利"。有价值，但不必神话
不止是数学家的焦虑
如果你觉得"证明消化不良"只是数学界的象牙塔问题，那就错了。
开源软件社区已经出现了同构的困境：AI批量生成的Pull Request涌入GitHub项目，维护者根本审不过来，部分项目被迫关闭外部PR通道。科幻杂志因AI投稿泛滥而暂停征稿。安全研究领域同样如此，过去声望给"发现漏洞的人"，现在AI扫描器一天发现的漏洞比过去一年还多，稀缺的变成了分诊和修复的人。
陶哲轩用五个字概括了这个时代的底层矛盾：生成便宜，验证贵。
这种焦虑有着现实根源，整个知识生产体系都面临生成式AI带来的代谢危机。
从警告到行动：一套建议
陶哲轩并非只抛出问题讲座后半部分给出了一系列建议：
第一，正常化披露 研究者应当公开说明自己使用了哪些AI工具、花了多少算力，无需因害怕被歧视而隐瞒。他自己的幻灯片脚注就写着："All em-dashes in these slides were human-generated"，这份学者式幽默也是身体力行。
第二，声望迁移 降低对"第一个生成证明的人"的过度崇拜，提高对消化、阐述、教学与经典化工作的声望权重。在丰裕时代，把知识讲清楚的人，应当和发现知识的人一样被尊重。
第三，制度跟上 国际数学联盟背书的《莱顿宣言》（Leiden Declaration on AI and Mathematics）已经在呼吁共同体主动定义规范，证明不仅给出确定性，也承载理解。
▲ 莱顿宣言网站列出给个人数学家的建议
十岁那年，陶哲轩在故乡阿德莱德与传奇数学家Paul Erdős合影。几十年后，Erdős留下的上千道开放问题成了AI"刷题"的公共靶场，而那个当年的天才少年，已经站在了裁判与守护者的位置。
他认可AI的能力和用途，同时提出：当证明从稀缺品变成过剩品，我们必须重新定义什么叫"解决了一个问题"。
否则，答案即使堆积如山，数学仍会淹没在自己的丰裕之中，因为那些答案无人理解。