AI证伪百年数学猜想被打假！Lean证明惊现漏洞，哥大教授破防了

新智元报道

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

编辑：大卫