近日，OpenAI宣称其新一代AI模型成功推翻了数学界著名的“Connes刚性猜想”，并公开了37000行Lean 4验证代码。然而仅24小时后，堪萨斯大学数学家J. L. Nielsen便发表论文驳回该结论。她逐行审查代码发现，AI构造的反例并未满足原猜想所需的附加条件。这意味着AI虽在形式上证明了每句话，但证明的陈述与原猜想无关，属于“对错误陈述的成功证明”。此次事件表明，机器只能验证逻辑形式，无法判断其是否契合人类意图，人类对AI科研结果的审查依然不可替代。目前，Connes刚性猜想仍保持开放状态。