AI 出的证明太多，也未必全是好事……数学界已经快读不过来了。

不过好消息是——

面对这场危机，两代菲尔兹奖得主，陶哲轩与王虹给出了几乎相同的判断：

消化。

北大数院最近释出了一篇王虹的万字专访长文，她给出了相当中肯的建议：

数学界不能忽略 AI 产生的反例或证明，我们需要去学习使用，也需要理解、消化。

陶哲轩则花了好几天时间，把一份由 AI 参与完成的证明，从头到尾消化了个遍。

这份证明解决的，正是悬置 67 年之久的森多夫猜想。

这听着多少有点反常识。既然 AI 是来帮数学家解题的，答案都出来了，为什么还要再消化一次？

「吹哨人」陶哲轩给出的答案是：

正确的证明，只是数学成果的第一关，它还要被专业数学家理解吸收，才能彻底可用。

打个比方，传统作者像负责到底的父母，完整陪伴一个证明从诞生到发表，而往后与 AI 共舞，这段关系可能更像「送养」：

有人借助 AI 把证明推进到生成或验证阶段，再正式交棒另一组人，进行专业阐释、整理和发表。

数学家依旧大有可为。

消化是解决数学百年危机的下一步

说白了，这也是陶哲轩在回应自己一个月前，在ICM 演讲中留下的问题：

如果答案可以被 AI 批量生产，数学研究究竟还要追求什么？

OpenAI 新模型 Astra 连破 10 道数学与理论计算机科学难题，横跨高维几何、编码理论、群论等多领域。

一位没有受过高等数学科班训练的神经外科医生，让 ChatGPT 5.6 自主运行约 16 小时，给出了数值线性代数中 Crouzeix 猜想的关键证明。

……

数学这堵高墙，眼看着被 AI 凿出了一扇后门。

连门外汉都能借它突破前沿难题，数学不会也要喜提 " 下一个土木 " 剧本吧？（doge）

非也！事实上，一项完整的数学成果从来不只有「得到证明」这一步。

陶哲轩把它拆成五段：

先生成论证，再核验正确；接着要把思路讲给同行听，让它经过发表和共同体检验；最后，还要把结果重新组织，找到它与旧理论的关系，沉淀成以后能调用的标准知识。

AI 目前最擅长加速前两步。越往后，就越需要数学家判断哪里才是核心，结果又意味着什么。

而陶哲轩刚处理的森多夫猜想，几乎是这段流程的 1 比 1 实战演练。

该猜想研究多项式零点与临界点的距离，此前较低次数和充分大次数都已经得到解决，中间范围仍然长期空悬。

几天前，数学爱好者 Lech Mazur 使用 AI 填补了这一缺口，并给出通过 Lean 验证的形式化证明。

似乎故事到这里就应该宣布结束了。但陶哲轩注意到，这份原始证明还没有被整理成适合人类阅读和发表的数学文本，也就是说，数学成果还不可用。

于是他花了数天，在 ChatGPT 和纸笔推导的共同辅助下，对成果进行了一次完整消化：

追溯文献来源→提炼真正起作用的恒等式→删掉绕路→把机器发现的论证改写成能看出主线的版本。

这一读，反而读出了些新东西。

整理后的论证不仅解决了 Sendov 猜想，还能覆盖更强的 Phelps – Rodriguez 猜想。所需的核心工具也比原始形式化呈现出来的要初等得多，Lean 代码从约 9 万行压缩至 1.5 万行。

换言之，消化不仅是对 AI 证明的再验证，也是拓宽数学成果的有效途径。

更重要的是，陶哲轩想借助消化，推翻数学界那套" 谁先宣布、谁获得优先权 "的旧规则。

数学成果的归属，最早看期刊发表日期，后来改看 arXiv 时间戳。

如今 AI 证明来得太快，连 arXiv 都有人嫌慢，一些结果刚生成就被扔上社交平台。为了抢先，验证阐释统统被跳过，最终给数学界人为制造了很多负担。

因此在 ICM 演讲中，陶哲轩主张，数学界不要再一味追捧「第一个给出证明的人」，应该提高「消化整理证明」的地位。

解释证明、审稿、把成果整理成经典理论，这些工作也要被重视，不能只有产出新定理才算功劳。

如果论文作者自己都没法做一场内行水平报告把结果讲明白，哪怕 AI 验证得再正确，这篇成果也不应该发表。

人都理解不了的证明，又怎么称得上完整成果。

所以陶哲轩呼吁学界都能冷静地坐下来，就 AI 的能力底线、数学的价值观来一场深刻的讨论，同时强调数学工作中那些无法被机器替代的部分。

One More Thing

与此同时，陶哲轩也实打实公开了一个面向 Lean 验证结果的登记库——Palomar。

Palomar 会把题目陈述、证明代码、AI 参与方式和版本信息登记清楚，再通过独立内核复核，将散落在 GitHub、社媒和新闻里的 AI 证明集合在一处。

它将作为验证与发表之间的消化中继站，让后来者知道 AI 和同行做到了哪里，还有哪些工作待完成。

对同一问题感兴趣的团队之间，可以通过 Palomar 合作研究。

值得注意的是，Palomar 不负责宣布某个结果有多重要，也不替代同行评审。

具体结果的归属权，未来将由四个时间节点的先后顺序共同决定：

记录证明如何产生的生成成果，如 AI 聊天记录；

确认逻辑正确的验证成果，如 Lean 代码；

把思路讲清楚的阐释成果，如公开演讲；

正式承载结果的发表成果，如论文。

中译中就是，谁先交齐一整套完整成果，谁才获得优先权。

目前，陶哲轩整理后的森多夫猜想，已经成为 Palomar 首批档案之一。

参考链接：

[ 1 ] https://arxiv.org/abs/2608.16753

[ 2 ] https://mathstodon.xyz/@tao/117123957813926355

[ 3 ] https://www.youtube.com/watch?v=M0--ZH1lOzg

[ 4 ] https://mp.weixin.qq.com/s/w-UfVMmwTZqXjNsC81CzYw

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

 量子位 AI 主题策划正在征集中！欢迎参与专题365 行 AI 落地方案，一千零一个 AI 应用，或与我们分享你在寻找的 AI 产品，或发现的AI 新动向。

也欢迎你加入量子位每日 AI 交流群，一起来畅聊 AI 吧～

一键关注 点亮星标

科技前沿进展每日见