Human paper says OpenAI’s 37,000-line Lean proof of Connes’ conjecture misses a key assumption

量子位 · wechat · 2026-08-04

OpenAI claimed its next-gen model had solved 10 world-class math problems, including Connes' rigidity conjecture. A subsequent human paper by J. L. Nielsen argues that the AI's alleged counterexample does not hold up after tracing OpenAI's 37,000-line Lean 4 proof back to the underlying mathematical objects.

What Nielsen found

He mapped the single-file Lean code back to the original math objects and identified two independent failure paths.
One key group in the AI proof appears not to satisfy the required assumptions: it is neither ICC nor does it have property (T).
Nielsen says the issue may be one of three things: a non-faithful formalization of property (T), a proof that only applies to a subcase but was lifted to the whole group, or a mismatch between the code and the written explanation.

Why this matters

The Lean kernel can verify that a proof is formally valid, but it cannot tell whether the statement actually matches the intended mathematical claim.
Nielsen formalized his rebuttal in Lean 4.32.2 as well, reinforcing the point that machine checking guarantees form, not meaning.
The paper places this in a broader context of prior verification failures, including empty theorems, bad axioms, and formally correct proofs of the wrong statement.

Connes' rigidity conjecture remains open.

Original post →

Human paper says OpenAI’s 37,000-line Lean proof of Connes’ conjecture misses a key assumption

More from Research