OpenAI 推理模型证明数学定理，Lean 验证遭内核漏洞质疑
OpenAI 推理模型证明量子并行重复定理，但人类难以理解证明；Lean 验证存在内核漏洞，科拉兹猜想证伪无效，凸显 AI 数学成果与形式化验证的局限。
OpenAI 内部推理模型宣布十项数学进展，包括首次证明量子并行重复定理——关于量子博弈中重复获胜概率衰减的定理。但哥大教授 Henry Yuen 指出，证明虽通过 Lean 形式化验证，关键步骤却难以理解。同时，一项用 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 和另外几个人一份论文草稿。 当时生活很忙，他无暇深入研读。现在，论文已经公布。他不吐不快，有话要说。