OpenAI's Connes Rigidity Disproof Looks Wrong on Inspection
For anyone not buried in operator algebra: Connes' Rigidity Conjecture says that if two essentially free, ergodic group actions produce isomorphic group measure space II₁ factors, then the actions are virtually conjugate and the groups are "similar" in a very strong way. It's a bridge between group theory and von Neumann algebras. A real disproof would be major, like "rewrite the chapter in every survey" major. So the burden of proof is enormous.
The open access PDF begins with the typical AI-era proof structure: definitions, lemmas, a counterexample construction, then a big claim. But the definitions aren't the problem. The problem is that the construction appears to violate ergodicity assumptions in order to get the algebra isomorphism to land. Without ergodicity, the group measure space factor decomposes as a direct integral over a non-transitive base, and the whole rigidity statement stops applying. It's not a counterexample to Connes; it's a counterexample to a strawman.
There's also a second issue hiding in the "isomorphism implies W-equivalence, therefore orbit equivalence" step. In some special families like Bernoulli actions, W-equivalence and orbit equivalence can be forced to coincide — that's precisely what makes rigidity theorems work. But that coincidence is not automatic. The PDF seems to assume that because two II₁ factors are isomorphic, their group measure space decompositions must align. That's a non-sequitur that pops up in amateur disproofs all the time. The algebra forgets a lot about the original action; bridging that gap is the actual difficulty.
I'm not saying the conjecture is definitely true. Sorin Popa's deformations/rigidity machinery has proven many special cases, and there are open directions where surprising counterexamples could exist. But this PDF isn't one. It commits the double sin of ignoring the technical setup and then treating the hardest part of the problem as a triviality.
If you're building an AI workflow for theorem proving — and I've been exploring Claude Code for formal proof assistance myself — this is a good cautionary case for prompt engineering. The model can produce a complete-looking document with lemmas and references. It can even name-drop. What it can't do is tell you when the conjecture's hypotheses have been conveniently contextualized away. The real skill is still human: checking whether every assumption is used, not just whether the syntax looks like math.
I'd love to see someone formally encode the conjecture in a proof assistant and let the AI search for counterexamples inside that bounded system. That would be genuinely useful. This PDF isn't that. It's a reminder that plausible, well-formatted mathematical prose is cheap — correctness is expensive.