Mathematicians Reject OpenAI's Claimed Conjecture Breakthrough Within 24 Hours

OpenAI said its next-generation model had solved ten world-class problems, including overturning the Connes rigidity conjecture. Within 24 hours, a human paper pushed back, arguing that the AI's counterexample does not hold.

The rebuttal comes from J. L. Nielsen of the Center for Topology and Physics at the University of Kansas. She traced OpenAI's publicly released 37,000 lines of Lean 4 code end to end, mapping every object back to its mathematical prototype, and identified two independent failure paths.

The Connes rigidity conjecture, proposed around 1980, asks whether two groups that generate identical algebraic structures must themselves be isomorphic once they satisfy two extra conditions — ICC and Kazhdan's property (T). To refute it, one must exhibit two non-isomorphic groups that satisfy both conditions and still produce the same algebra.

That is what OpenAI's model claimed to do: it constructed two non-isomorphic groups generating the same algebra, with proofs that both satisfy ICC and property (T). The entire argument was written as 37,000 lines of Lean 4 code, verified line by line by the Lean kernel, plus a document explaining how the groups were built.

Nielsen argues that one of the AI-constructed groups in fact fails the extra conditions — it is neither ICC nor property (T). She lists three possibilities: the code's property (T) does not faithfully match Kazhdan's original definition; the proof holds only for part of the group but was applied to the whole; or the group in the code is not the one described in the document.

Because the released code is a single merged file with all module-level names stripped, she built a mapping table labeling every object's name and line number: the cocycle group at line 13,700, the twisted group at line 14,069, the algebra-isomorphism proof at line 36,712, and the main theorem at line 36,954. Tracing the ICC proof chain, she found the lemmas handle objects after a dual transformation rather than the original group with its central element, so they do not directly cover the critical elements.

For Nielsen, the problem is what is being proved, not whether the proof is correct — Lean only verifies the latter. She compiled her own two counterarguments as Lean code under Lean 4.32.2. The paper's final section broadens the point: the Lean kernel guarantees a proof is formally seamless, but not that it proves the original claim. As Terence Tao has put it, verification confirms the formal statement itself, not that the statement matches intent, so human review cannot be replaced.

Such incidents have a record: an audit of five common Lean benchmarks produced 4,833 findings — counterexamples, vacuous theorems, and unreliable axioms — all machine-verified, until humans constructed counterexamples and found the proved statements themselves were wrong. In formalized statistical learning theory, the worst case has been described as "not a failed proof, but a successful proof of a wrong statement."

Nielsen writes that OpenAI's formalization may have correctly established every conclusion it claims; what it did not establish — and what the Lean kernel cannot check — is whether those conclusions relate to the original wording of the conjecture. A human reading the conjecture sees the premises; a proof assistant given a conclusion that fails the premises will happily verify any assertion about it. The Connes rigidity conjecture remains open.