从OpenAI到科拉兹猜想：AI数学证明的人类角色

算力再强，也证不出错误的定理

据行业观察，OpenAI内部最新的推理模型，在数学领域取得了多项突破性进展，涵盖多个长期悬而未决的经典问题，其中包括：

• 首次证明了非Sofic群的存在性
• 给出了全新的电路下界理论
• 攻克了最近向量问题的难度极限
• 完成双人量子博弈并行重复指数衰减定理的证明

哥伦比亚大学计算机科学副教授Henry Yuen对最后一项成果尤为关注。早在2016年，他就在该问题上取得了关键性进展，但始终未能完成最终的完整证明。在接下来的十年里，他多次尝试冲击这一难题，甚至在一个月前借助ChatGPT 5.5重新展开研究，却始终未能取得实质性突破。而AI最终在他此前的研究基础上，完成了这一困扰他多年的证明。

几天前，Lijie Chen向Henry Yuen等人分享了这份论文草稿，当时Yuen因事务繁忙未能深入研读，如今论文正式公布，他忍不住分享了自己的感受。

量子并行重复定理是Henry Yuen在研究生时期耗费数年心血钻研的领域，也是他最引以为傲的研究成果。他至今仍记得那些泡在咖啡馆的午后、办公室的深夜，以及无数个本该休息的周末，反复拆解研读Ran Raz的经典并行重复定理，只为攻克该问题的量子版本。最终他成功证明了多项式衰减的结论，也借此建立了对自身研究能力的信心，确认自己能够解决那些学界关注的重要问题。

Yuen相信OpenAI的这份证明是正确的，毕竟已经有Lean形式化验证通过。但要完全消化这份新证明，他还需要花费不少时间。尽管新证明确实从他此前止步的地方继续延伸，但AI突破了他原有证明策略的限制，使用了一些算子理论和泛函分析领域的研究者早已掌握的技巧。

兴奋之余，Yuen首先对论文的写作风格感到失望。他表示这份证明充满了AI生成的典型特征：冗长的铺垫绕了许久，关键环节却如同变魔术般突兀，让人摸不着头脑。

OpenAI的证明读起来既有趣又令人头疼：它先将问题清晰地摆在面前，随后突然跳转至“用预解式寻找正确的purification”的方向，中间几乎没有任何逻辑过渡。接下来是一连串非常规的矩阵熵计算，绕了许久后才得出“这条路可行”的结论，但最关键的一步，也就是这一证明的核心直觉来源，却没有任何解释。

而整篇证明中最精妙、最考验创造力的环节——利用Uhlmann变换进行算子空间膨胀的技巧，本应是全文的高潮，却被AI毫无预警、不加解释地放在了第四节，仿佛随手丢弃的泥沙。正确的证明却隐藏了最重要的核心想法，Yuen希望OpenAI能进一步优化文稿的逻辑梳理。

更让人感慨的是第二层认知：Lean验证通过，不等于真正理解。机器可以保证每一步推导都无懈可击，但诸如“为什么这一方法有效”“它在更大的理论版图中意味着什么”“还能应用在哪些场景”这类问题，Lean完全无法给出答案。Yuen坦言，他目前仍在逐步消化这份证明，只能像阅读外行的论文一样，逐行还原AI没有明确说明的核心直觉。

AI确实拓宽了人类理解的疆域，但随之而来的问题也接踵而至：研究的乐趣和意义还剩什么？如果AI解决了所有自己魂牵梦绕的难题，自己还能剩下什么？Yuen越来越确定，数学家接下来的日子不会清闲，既要驯服这些AI生成的“思想巨兽”，还要把其中的专业黑话翻译成人类能理解的语言。

AI「证伪」百年数学猜想被打假！Lean也不是保险箱

上周，有研究者Ramana Kumar用300行Lean代码尝试证伪最知名的数学未解之谜——科拉兹猜想。这个猜想的内容十分简单：对于任意正整数，按照“偶数除以2，奇数乘以3再加1”的规则反复操作，最终是否都会落入4→2→1的循环？

自1937年数学家Lothar Collatz提出该猜想以来，学界既无法证明其成立，也未找到反例。数学家Paul Erdős曾评价“数学还没准备好应对这样的问题”，美国科学院院士Jeffrey Lagarias也认为“这是个异常困难的问题，完全超出了当今数学的范围”。如果该猜想被证伪，无疑会是数学界的爆炸性新闻。

但仅三天后，这份形式化的Lean证明就被判定为无效，因为它实际上利用了Lean内核的一个底层漏洞。OpenAI的Daniel Selsam带领一个专攻网络安全方向的AI团队协助Lean FRO进行内核审计，结果发现了不止一处系统漏洞。

几乎与此同时，罗格斯大学数学教授、Lean专项研究组织顾问Alex Kontorovich发文提醒，不要将Lean视为全能验证工具。他直指形式化数学的核心死穴——语义对齐问题：即使Lean内核本身没有任何问题，它也只能保证代码编译通过、形式逻辑正确，但无法确保你在代码中定义的概念，和人类用自然语言表达的直觉意图完全一致。

Lean能确认的只有一件事：代码的形式推导没有错误，但它绝不验证一个更致命的问题：这段形式化陈述，真的对应你想要证明的那个数学定理吗？哪怕定理的推导完全正确，但如果题目理解错了，Lean依然会通过验证。而这种语义对齐的问题，无法单纯依靠计算机解决。

Kontorovich在ICM 2026的演讲中就曾指出，形式化数学最大的盲区，不在于“推导是否正确”，而在于“表达是否准确”，最终的把关依然需要人类专家。当年Liquid Tensor Experiment能够获得学界认可，恰恰源于研究者对每个数学定义近乎严苛的人工审查。

综合来看，这两件事指向同一个核心事实：AI可以完成数学证明，机器可以验证形式逻辑，但理解证明的内涵、把关研究的准确性，依然是人类的工作。

最后，关于AI推理模型还有一则值得关注的细节：AI生成的证明虽然在形式上正确，但其中蕴含的核心直觉往往隐藏在复杂的推导过程中，人类研究者需要花费大量时间去还原和理解这些内容。