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

8月4日下午消息，OpenAI此前宣称下一代AI模型Astra解决了10个世界级数学难题，其中包括推翻了有40余年历史的Connes刚性猜想，并公开了37000行Lean 4形式化证明代码。然而仅24小时后，堪萨斯大学拓扑物理中心数学家J. L. Nielsen就发布论文，指出AI提出的反例不成立。

事件核心经过

• OpenAI宣称突破：OpenAI新模型构造了两个不同构的群，声称它们生成相同的冯·诺依曼代数，且均满足ICC条件和Kazhdan性质(T)，以此推翻Connes刚性猜想
• 数学家逐行核验：Nielsen将37000行单文件Lean代码从头追到尾，为每个数学对象制作了名称与行号对照表，从零上闭链群到主定理逐一核对
• 发现关键错误：AI构造的其中一个群实际上既不是ICC群，也不满足Kazhdan性质(T)，证明的引理处理的是经过对偶变换后的对象，并未直接覆盖关键元素
• 形式正确但命题错误：Lean内核只验证证明形式上的正确性，不负责检查被证明的命题是否与原猜想的前提条件相符

AI科研的启示

这一事件深刻揭示了当前AI辅助数学研究的本质局限：

1. 形式验证不等于语义验证：定理证明器能保证每一步推理在逻辑上严丝合缝，但无法判断被证明的陈述是否就是研究者最初想要证明的那个命题
2. 人类审查不可替代：正如陶哲轩所言，验证证明的是形式陈述本身，而不是这个陈述和意图相符，人类数学家的语义审查无法直接被机器取代
3. 历史已有先例：此前针对五个常用Lean基准的审计就发现了4833条问题，包括反例、空洞定理和不可靠公理，全都通过了机器验证

Connes刚性猜想提出于1980年左右，猜测满足ICC和Kazhdan性质(T)两个条件的群，如果其冯·诺依曼代数同构，则群本身必须同构。截至目前，这一猜想仍然开放，AI的"突破"被证明是一次对错误命题的成功证明。

Nielsen将自己的两条独立反驳路径也写成了Lean代码，并在Lean 4.32.2下编译通过。这一事件再次证明，在基础科研领域，AI目前更适合作为数学家的辅助工具，而非独立的问题解决者。