北京
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]
文章来源：量子位。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
