数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”

正文
OpenAI近日高调宣布，其下一代AI模型解决了10个世界级难题，其中最引人注目的成果是“推翻”了由数学家Alain Connes在1980年左右提出的Connes刚性猜想。这一猜想的核心是：只要一个群满足ICC和Kazhdan性质(T)这两个附加条件，其配对的代数结构若相同，则群本身也必须相同。OpenAI的模型试图通过构造两个不同构但代数结构相同的群来反驳该猜想，并生成了长达37000行的Lean 4形式化证明代码以支撑其结论量子位。

然而，这一看似突破性的成果在24小时内便遭到人类数学家的有力驳回。堪萨斯大学拓扑物理中心的J. L. Nielsen对OpenAI公开的全部代码进行了详尽审查，将代码中的每一个对象逐一映射回其数学原型。最终，Nielsen发现AI提出的反例存在两条互相独立的失败路径，其核心问题在于：AI虽然在形式化证明中“证对了每一句话”，但其构造的数学对象实际上并未满足猜想所需的前提条件，因此整个反例与Connes刚性猜想本身并无实质关联搜狐。这一发现直接宣告了AI此次“攻破”猜想的无效。

这一事件清晰地揭示了当前AI在数学研究中的能力边界与风险。大型语言模型或专用AI系统能够熟练地生成符合语法规范的形式化证明代码，甚至通过形式化验证器的检查，但这并不等同于进行了有意义的数学推理。AI可能会在未完全理解问题本质的情况下，构造出看似自洽但实则偏离原始定义的论证。正如Nielsen的工作所展示的，人类专家对AI产出进行严格的语义审查和概念溯源，是确保科研严谨性的最后一道、也是至关重要的防线搜狐。

此次“24小时驳回”事件，为AI for Science的热潮提供了一个冷静的注脚。它表明，即便AI能够辅助处理复杂的符号推理，但其成果的可靠性仍需由领域专家进行深度验证。未来，人类数学家与AI的关系更可能是一种紧密协作：AI负责探索海量的可能性空间并生成候选证明，而人类则凭借深刻的领域洞察力，负责提出关键问题、审视证明逻辑的真伪，并最终判定一项猜想是否被真正解决。原文未提供更多关于OpenAI对此驳回回应的信息。