AI 生成的数学证明越来越多，数学界面临的新问题已不只是「能不能做出来」，而是「读不读得过来、用不用得起来」。围绕这一点，两代菲尔兹奖得主陶哲轩与王虹给出了近乎一致的判断：面对 AI，数学界需要学会消化。
北京大学数学科学学院近日释出一篇王虹的万字专访。她在文中提到，数学界不能忽略 AI 产生的反例或证明，既要学习使用，也要理解、消化。
陶哲轩的对应做法更直接。他花了几天时间，把一份由 AI 参与完成的证明从头到尾重新梳理了一遍。这份证明解决的是悬置 67 年的 Sendov 猜想。
证明出来，不等于成果已经可用
在陶哲轩看来，正确的证明只是数学成果的第一关。一个结果要真正进入数学共同体，还需要被专业数学家理解和吸收，之后才能成为可用的知识。
按照文中的比喻，传统作者像全程负责的父母，从证明诞生一路陪伴到发表；而在 AI 参与更深的情况下，这种关系可能更像「送养」：有人借助 AI 把证明推进到生成或验证阶段，再交由另一组人完成专业阐释、整理和发表。
这也意味着，数学家的工作并没有被拿走，而是更集中地转向后续环节。
陶哲轩把数学成果拆成五个阶段
这一判断，也是陶哲轩对自己一个月前在 ICM 演讲中所提问题的回应：如果答案可以被 AI 批量生产，数学研究还应追求什么。
文中提到，OpenAI 新模型 Astra 连续解决 10 道数学与理论计算机科学难题，涉及高维几何、编码理论、群论等多个方向。另一例子是，一名没有受过高等数学科班训练的神经外科医生，让 ChatGPT 5.6 自主运行约 16 小时，给出了数值线性代数中 Crouzeix 猜想的关键证明。
在这样的背景下，陶哲轩把一项完整的数学成果拆成五段：
- 生成论证；
- 核验正确；
- 把思路讲给同行听；
- 经过发表和共同体检验；
- 重新组织结果，找到它与旧理论的关系，沉淀为以后可调用的标准知识。
按他的判断，AI 目前最擅长加速前两步。越往后，越需要数学家判断什么才是核心，以及结果究竟意味着什么。
Sendov 猜想成为一次完整的“消化”实战
Sendov 猜想讨论的是多项式零点与临界点之间的距离。文中称，此前较低次数和充分大次数的情形已经得到解决，但中间范围长期悬而未决。
几天前，数学爱好者 Lech Mazur 使用 AI 填补了这一缺口，并给出了一份通过 Lean 验证的形式化证明。表面上看，问题似乎已经结束；但陶哲轩注意到，这份原始证明还没有被整理成适合人类阅读和发表的数学文本，换句话说，这项成果还不能直接使用。
于是，陶哲轩在 ChatGPT 和纸笔推导的共同辅助下，花了数天时间做了一次完整整理：追溯文献来源、提炼真正起作用的恒等式、删去绕路步骤，再把机器发现的论证改写成能看出主线的版本。
这一轮整理之后，结果不只停留在复述原证明。文中称，整理后的论证不仅解决了 Sendov 猜想，还能覆盖更强的 Phelps–Rodriguez 猜想；所需的核心工具也比原始形式化版本显示出来的更初等，Lean 代码量从约 9 万行压缩至 1.5 万行。
按照这一案例，所谓消化，并不只是对 AI 证明再做一遍确认，也可能成为拓宽数学成果的一步。
优先权规则可能要变
陶哲轩还试图借「消化」重新讨论数学界的优先权规则。
过去，数学成果归属最早看期刊发表日期，后来更多转向 arXiv 时间戳。现在 AI 证明出现得更快，文中提到，连 arXiv 都有人嫌慢，一些结果刚生成就被发布到社交平台。为了抢先，验证和阐释被跳过，也给数学界制造了额外负担。
因此，陶哲轩在 ICM 演讲中主张，数学界不应只追捧「第一个给出证明的人」，而应提高「消化整理证明」的地位。解释证明、审稿、把成果整理成经典理论，这些工作都应被纳入评价，而不是只有产出新定理才算贡献。
按照文中的表述，如果论文作者自己都无法做一场面向内行的报告，把结果讲清楚，那么即便 AI 已经验证其正确性，这篇成果也不应发表。
在他看来，连人都无法理解的证明，很难算作完整成果。为此，他呼吁学界围绕 AI 的能力边界和数学的价值观展开更深入讨论，同时明确那些仍无法被机器替代的工作。
Palomar 作为验证与发表之间的中继站
除了公开表态，陶哲轩也推出了一个面向 Lean 验证结果的登记库 Palomar。
根据文中介绍，Palomar 会登记题目陈述、证明代码、AI 参与方式和版本信息，并通过独立内核复核，把分散在 GitHub、社交平台和新闻中的 AI 证明集中到同一处。
它被设计为验证与发表之间的「消化」中继站，让后来者知道 AI 和同行已经推进到哪一步，以及还有哪些工作尚待完成。对同一问题感兴趣的团队，也可以通过 Palomar 开展合作研究。
不过，Palomar 不负责宣布某个结果有多重要，也不替代同行评审。
关于未来的成果归属，文中称，具体优先权将由四个时间节点的先后顺序共同决定：
- 记录证明如何产生的生成成果，例如 AI 聊天记录；
- 确认逻辑正确的验证成果，例如 Lean 代码；
- 把思路讲清楚的阐释成果，例如公开演讲；
- 正式承载结果的发表成果，例如论文。
按照这一套说法，谁先交齐一整套完整成果，谁才获得优先权。
目前，陶哲轩整理后的 Sendov 猜想，已经成为 Palomar 首批档案之一。