OpenAI 新模型数学证明翻车：24小时内被人类数学家驳回

JFPuget · x · 2026-08-07

OpenAI 此前宣称其下一代 AI 模型解决了 10 个世界级数学难题，其中包括用 37,000 行 Lean 4 代码“推翻了 Connes 刚性猜想”。然而不到 24 小时，堪萨斯大学的数学家 J. L. Nielsen 就发表论文反驳了这一结论。

Nielsen 逐行追踪了代码库，指出 AI 构造的反例并不成立：其中一个群未能满足猜想所要求的 ICC 和 Kazhdan 性质(T) 条件。这证明了代码虽然通过了形式化验证，但在对应高阶数学定义时存在偏差。该事件再次凸显了在复杂的 AI 科研产出中，人类审查依然不可或缺。