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

TL;DR - OpenAI claimed its next-gen model disproved the Connes rigidity conjecture with a 37,000-line Lean 4 formal proof, but within a day mathematician J. L. Nielsen (University of Kansas) published a rebuttal arguing the constructed counterexample fails the conjecture's hypotheses — so the conjecture remains open.

• Connes' rigidity conjecture states that for groups satisfying ICC and Kazhdan property (T), the associated algebra determines the group; refuting it requires two non-isomorphic groups meeting both conditions that generate the same algebra.
• Nielsen mapped the single-file released Lean code back to its mathematical objects line-by-line (cocycle group ~L13700, twisted group ~L14069, algebra isomorphism ~L36712, main theorem ~L36954) and gave two independent failure paths, arguing one of the AI's groups satisfies neither ICC nor property (T).
• The ICC reasoning chain (L31430–31610) allegedly operates on dualized objects rather than the original group with its central element, so it never covers the critical elements; Nielsen formalized her own rebuttal in Lean 4.32.2.
• Core lesson: Lean's kernel verifies formal correctness, not whether the formal statement matches the intended claim — echoing Terence Tao's point, and prior audits of five Lean benchmarks that surfaced 4,833 issues (counterexamples, vacuous theorems, unsound axioms) that all passed machine checking.