OpenAI内部最新推理模型,一口气发布了十项惊人的数学进展。
其中包括:
- 首次证明了非Sofic群(Non-sofic groups)的存在性 ;
- 给出了全新的电路下界(Circuit lower bounds);
- 攻克了最近向量问题(Closest Vector Problem,CVP)难度极限;
- 以及双人量子博弈并行重复指数衰减定理(Quantum parallel repetition)。
最令哥伦比亚大学副教授Henry Yuen在乎的是最后一个——
2016年,Yuen在该问题上取得了重大进展,但并未彻底解决。10年来,他屡战屡败,甚至一个月前他还用ChatGPT 5.5再次向终极证明冲锋,但收获寥寥。
而AI在他的肩膀上,轻轻一脚,把球送进了球门。
证明对了,人类却没理解
几天前,Lijie Chen发给Henry Yuen和另外几个人一份论文草稿。
当时生活很忙,他无暇深入研读。现在,论文已经公布。他不吐不快,有话要说。
量子并行重复定理(Quantum parallel repetition theorem),是Henry Yuen在研究生阶段耗费数年心血钻研的领域,也是他最引以为傲的成果。
Henry Yuen,现任哥伦比亚大学Srivani Family计算机科学副教授
他记得那些泡在咖啡馆里的午后,坐在办公室里的深夜,还有无数个本该休息的周末,反复拆解研读Ran Raz的经典并行重复定理。
他想解决这个定理的量子版本,为此夜不能寐、辗转反侧。他吞下了成吨的数学工具,最终成功证明了多项式衰减。
https://arxiv.org/pdf/1604.04340
更重要的是,他从中建立了信心,终于认清自己的实力,证明了他确实能解决那些(至少一部分)别人也在乎的问题。
他相信OpenAI的这份证明应该是正确的,毕竟已经有Lean形式化证明。但要消化这个新证明,Henry Yuen还需要一些时间。
虽然新证明确实从他之前结束的地方继续出发,但AI突破了他原有证明策略的限制,使用了一些技巧和方法。这些方法或许已经被算子理论(operator theory)和泛函分析(functional analysis)领域的研究者所掌握。
兴奋之外,Yuen的第一个感受是失望,对论文写作风格的失望。
他说这份证明读起来满是AI味儿:冗长的铺垫绕了半天,关键环节却像变魔术,让人一头雾水。
OpenAI的证明,读来颇有意思,却也有些令人头疼。
它先把问题端端正正地摆在桌上,然后忽然一跃到「用预解式去找正确的purification」这个方向,中间几乎不留任何逻辑阶梯。
接下来,便是一连串颇为另类的矩阵熵计算,弯弯绕绕地算下去,末了告诉你:这条路走得通。
可那最关键的一步,那个直觉究竟从何而来,它没有说。
而最精妙、最考验创造力的那一笔——利用Uhlmann 变换(Uhlmann transformation) 进行算子空间膨胀的技巧,本应是整篇证明最动人心魄的高潮,却被AI弃子如泥沙,毫无预警、毫无解释地丢在了第四节。
正确的证明,却藏起来了最重要的想法。
他希望OpenAI能多花几个提示词,把这篇文稿好好理一理。
更扎心的是第二层:Lean验证通过,不等于理解。
机器可以保证每一步推导无懈可击,但「为什么这一招有效」「它在更大的理论版图里意味着什么」「还能用在哪里」——这些问题,Lean一个都答不了。
Yuen坦言,他到现在还在消化这份证明。
答案摆在面前,他却要像读外行的论文一样,一行行去还原AI没说出口的直觉。
没错,是有个Lean证明在那儿。可那只是形式化,不代表我懂了。真要消化,恐怕只能靠时间慢慢磨。
的确,AI拓宽了人类理解的疆域,但然后呢?研究的乐趣和意义还剩什么?要是AI把他魂牵梦绕的难题都解决了,他还剩什么?
问题接踵而至。但有一点他越来越确定:数学家接下来的日子不会闲,既要驯服这些思想巨兽,还得把它们的黑话翻译成人话。
AI「证伪」百年数学猜想被打假!Lean也不是保险箱
上周,Ramana Kumar用300行Lean证伪了最出名的数学未解之谜「科拉兹猜想」(Collatz conjecture)。
它问的问题特别简单:给你一个正整数,按两条规矩反复操作——偶数就除以 2,奇数就乘以3再加1——最后是不是不管从哪个数出发,都会一路跌到1?
你可以算一下:
这个猜想说的就是:不管你拿哪个正整数开头,最后都会掉进这个 4→2→1 的圈里。
这个问题自数学家Lothar Collatz在1937年提出后,没有人能证明它成立,也没有找到反例。
它被数学家Paul Erdős称为:「数学还没准备好应对这样的问题」,而美国科学院院士、数学家Jeffrey Lagarias则认为「这是个异常困难的问题,完全超出了当今数学的范围」。
如果被证伪,无疑是数学界爆炸性新闻。
可惜的是,3天后,这份形式化的Lean证明被判无效,因为它实际上只是利用了Lean内核的一个底层漏洞。
OpenAI的Daniel Selsam,带着一个专攻网络安全方向的 AI,协助Lean FRO做了一次内核审计。
结果,他们在Lean内核里发现了不止一起漏洞!
几乎同一时间,Rutgers大学数学教授、Lean专项研究组织顾问Alex Kontorovich发文提醒:别把Lean当全能验证者。
他直指死穴——语义对齐(Semantic Alignment)。
即使Lean内核无懈可击,Lean也只管代码编译。谁来确保你写在代码里的「定义」和人类在自然语言里的「直觉意图」是一回事?
Lean能确认的只有一件事:代码编译通过,形式逻辑无误。但它绝不验证一个更要命的问题:这段形式化陈述,真的对应你想证的那个定理吗?
定理证对了,题目抄错了,Lean照样绿灯放行。
而这个对齐问题,没法纯靠计算机解决。
在ICM 2026的演讲里,Kontorovich就点过:形式化数学最大的盲区,不在「推对了导」,而在「说对了话」。最后把关的,还得是人类专家。
当年Liquid Tensor Experiment之所以封神,靠的恰恰是研究者对每个数学定义近乎偏执的人工审查。
把两位教授的话放在一起看,指向同一个事实:AI能证明,机器能验证,但理解和把关,还是人类的活。
最后,还有个关于AI推理模型的八卦:
参考资料:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
本文来自微信公众号“新智元”,作者:ASI启示录;编辑:大卫
