OpenAI宣称其新一代AI模型通过形式化验证解决了包括Connes刚性猜想在内的十个世界级难题 [1]。然而，堪萨斯大学数学家J. L. Nielsen在24小时内通过逐行分析37000行Lean 4代码，发现了这一证明的关键漏洞 [1]。Nielsen指出，AI构造的其中一个群并未满足猜想要求的两个附加条件——ICC和Kazhdan性质T [1]，证明OpenAI声称的反例实际上不成立 [1]。
Nielsen通过对照表将代码中的数学对象一一标出，包括零上闭链群在第13700行和主定理在第36954行 [1]。他发现证明过程处理的是经过对偶变换之后的对象，而非原来那个带中心元素的群 [1]。这表明虽然AI在形式层面通过了机器验证，但实际上改变了问题的本质。Nielsen甚至将自己的反驳也写成了Lean代码在Lean 4.32.2下编译 [1]。
Nielsen强调，机器验证只能检查形式正确性，无法验证证明内容与原猜想的关联性 [1]。他引用陶哲轩的观点指出，验证的是形式陈述本身，而不是这个陈述与意图是否相符 [1]。过往的Lean基准审计发现了包括反例、空洞定理和不可靠公理在内的4833条问题，这些都通过了机器验证 [1]，进一步证明了形式验证的局限性。
OpenAI announced that its next-generation AI model had solved ten world-class mathematical problems, including disproving the Connes rigidity conjecture through formal verification [1]. However, mathematician J. L. Nielsen from the University of Kansas challenged this claim by conducting a line-by-line analysis of 37,000 lines of Lean 4 code within 24 hours [1]. Nielsen discovered that the group constructed by the AI failed to satisfy two essential conditions required by the conjecture: the ICC (infinite conjugacy classes) property and Kazhdan property (T) [1].
Nielsen's investigation revealed a fundamental flaw in the AI's reasoning [1]. The mathematical objects processed in the proof were derived through a dual transformation, meaning they no longer represented the original group containing the central elements specified in the conjecture [1]. By mapping code elements to their corresponding mathematical objects—such as locating zero-closed chain groups at line 13,700 and the main theorem at line 36,954—Nielsen demonstrated that OpenAI's purported counterexample did not actually constitute a valid refutation [1].
This discrepancy highlights a critical limitation of machine verification [1]. Formal verification can only validate the internal logical consistency of a proof statement itself, not whether that statement aligns with the original conjecture's intent [1]. Past Lean audits identified 4,833 issues including false counterexamples, vacuous theorems, and unreliable axioms—all of which had passed machine verification [1]. To reinforce his findings, Nielsen also formalized his refutation as Lean code, compiling it successfully under Lean 4.32.2 [1].
