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
本文来自微信公众号“量子位”,作者:关注前沿科技
