陶哲轩隔空对话王虹：数学界该学会“消化”AI了

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

本文来自微信公众号“量子位”，作者：关注前沿科技，36氪经授权发布。