陶哲轩与王虹对话：数学界该如何「消化」AI 生成的证明

两位菲尔兹奖得主陶哲轩与王虹近期分别发声，呼吁数学界正视 AI 批量生成证明带来的冲击，把「消化」AI 成果作为下一步研究重点。陶哲轩同步上线了面向 Lean 验证结果的登记库 Palomar，并提出按四阶段重新定义数学成果的优先权归属规则。

AI 证明激增，数学界快读不过来了

最近一段时间，AI 辅助数学证明的进展接连引爆话题：OpenAI 新模型 Astra 连破 10 道数学与理论计算机科学难题；一位未受数学科班训练的神经外科医生借助 ChatGPT 自主运行约 16 小时，给出 Crouzeix 猜想的关键证明。这些案例在让人振奋的同时，也给数学共同体带来新负担——AI 产出的证明数量飙升，但很多成果既未经过同行阐释，也未被整理成可发表、可引用的文本。

北大数院近期释出王虹的万字专访，王虹直言：数学界不能忽略 AI 产生的反例或证明，需要学习使用，也需要理解、消化。这一观点与陶哲轩几乎完全一致。

把数学成果拆成五段，消化是最后一公里

陶哲轩在 ICM 演讲中提出，完整的数学成果需经历五个阶段：

• 生成论证
• 核验正确
• 阐释给同行
• 经发表与共同体检验
• 与旧理论衔接，沉淀为可调用的标准知识

AI 最擅长加速前两步，但从第三步起，越往后越需要数学家判断哪里是核心、结果意味着什么。

陶哲轩近期处理的森多夫猜想（Sendov's conjecture）正是这一流程的实战样本。该猜想研究多项式零点与临界点的距离，较低次数和充分大次数的情况此前已解决，中间范围空悬 67 年。几天前，数学爱好者 Lech Mazur 用 AI 填补了这一缺口，并给出通过 Lean 验证的形式化证明。

但这份证明的原始版本还未被整理成人类可读、可发表的数学文本。于是陶哲轩花了数天，借助 ChatGPT 与纸笔推导，对成果做了一次完整「消化」：追溯文献来源 → 提炼真正起作用的恒等式 → 删掉绕路 → 把机器论证改写成能看出主线的版本。

这次消化还带来了意外收获：整理后的论证不仅解决了森多夫猜想，还能覆盖更强的 Phelps–Rodriguez 猜想；所需核心工具也更为初等，Lean 代码从约 9 万行压缩至 1.5 万行。

上线 Palomar，重新定义成果归属

陶哲轩同步公开了一个面向 Lean 验证结果的登记库 Palomar，会把题目陈述、证明代码、AI 参与方式和版本信息登记清楚，再通过独立内核复核，把散落在 GitHub、社媒和新闻里的 AI 证明集合在一处，作为验证与发表之间的「消化中继站」。

Palomar 不替代同行评审，也不评价结果重要性。具体成果的归属权，将由四个时间节点的先后顺序共同决定：

• 生成成果：记录证明如何产生，如 AI 聊天记录
• 验证成果：确认逻辑正确，如 Lean 代码
• 阐释成果：把思路讲清楚，如公开演讲
• 发表成果：正式承载结果，如论文

简言之，谁先交齐一整套完整成果，谁才获得优先权。目前，陶哲轩整理后的森多夫猜想已成为 Palomar 首批档案之一。

数学研究还要追求什么

陶哲轩主张，数学界不应再一味追捧「第一个给出证明的人」，而应提高「消化整理证明」的地位——解释、审稿、把成果整理为经典理论的工作同样重要。如果论文作者自己都没法做一场内行水平的报告把结果讲明白，哪怕 AI 验证再正确，成果也不应发表。

这与王虹的呼吁形成呼应。两人从不同角度，共同指向一个核心问题：当 AI 可以批量生产证明，数学研究究竟还要追求什么？答案或许是——人能否真正理解、并向他人讲清楚这些证明。