OpenAI's claimed disproof of Connes' Rigidity Conjecture is invalid [pdf]
philarchive.orgThe author of this paper has also apparently published a proof of the Riemann Hypothesis. yeah idk if they should be trusted as an authority on this.
From what I can tell it seems like they are probably wrong, but a mathematician publishing a paper about a well known unsolved problem in mathematics does not indicate they are a crank, even if their paper is wrong. This is a thing respected researchers in mathematics do.
link for the curious https://philarchive.org/archive/NIEPOT-5
Crank author at a crank “institution” - I can’t assess whether the OpenAI paper is accurate but I highly doubt this is going to be the paper to disprove it.
University of Kansas is not a crank institution. Author has MS and MA from KU and BSc summa cum laude / Valedictorian of her departments from UMKC. Trying to call her a crank for hosting a private think tank is jealous nonsense.
Author is a crackpot. She does not meaningfully engage with anyone who points out the key flaw in her counterargument. See the thread here https://x.com/AcerFur/status/2083649346294382803
Thanks — sorry for spreading nonsense.
The nonsense is the crackpot who wrote this evaluation. Nielsen is an established physicist close to completing two PhDs.
Author is a PhD candidate who graduated summa cum laude in BSc Physics Valedictorian of her college and math with double master's degrees. You're the crackpot clearly, you provide no correct disproof of Nielsen.
This is complete nonsense accusation. She disproved Acerfur completely.
Maybe there's an error, but much of this write-up reads like nonsense to me. The assertion that a semidirect product with an abelian factor must admit that factor in its center is absolutely false. This is actually acknowledged later in this article, but is handwaved away in incomprehensible fashion.
Nielsen is an expert, not a crank. She worked at I2S at the University of Kansas and passed her master's and her PhD thesis in PhilSci / PhiLMath is on the web and completely airtight.
Genuine question - this is so hard for me to follow. Not that I could follow the original disproof anyways. But how is "truth" determined when the effort required to validate is so high?
It's a common problem in math. The famous proof for Fermat's last theorem took 2 years to validate.
That's different though. Understanding the spec of Fermat's last theorem is simple. Here, you already need to know some mathematics just to understand the spec.
These AI generated proofs have something akin to the quantum algorithms that can generate a response that would take 1 billion years of processing to finish on a classical computer. How do you test them to see if the result was correct?
No they don't. They have a few thousand lines and the hinge points are easy to find. This is more nonsense.
One of mathematicians working at OpenAI refuted those claims directly on X - https://x.com/AcerFur/status/2083656978719719601
Good grief that thread is sad, with it ending by Gary Marcus asking for the crank to be taken seriously.
This "paper" itself is 100% AI-generated...
What makes you say that? Not dunking, I skimmed it (I’m in no way at this level) and didn’t see anything outright Claud-y.
This immediately struck me as Claud-y:
> The gap has two independent consequences, each sufficient to invalidate the claimed disproof. The first is structural.
Then the classic coding agents negation of earlier evidence, instaed of just updating to use new references, they mention that they changed old to new:
> The publicly released monolithic file ConnesRigidity.lean (37,000+ lines) does not use the names CocycleExtension, ZeroCocycle, or TwistedCocycle that appeared in the earlier modular source files (CocycleExtension.lean, ICC.lean, CrossedClosure.lean). However, the identical mathematical construction is present under different names. The following table gives the correspondence, with line numbers in the published file.
> This is the same zero-cocycle / twisted-cocycle structure identified in the earlier modular source files, confirming that the structural analysis of this note applies to the published code
And some other Claud-y stuff:
> Why both paths are closed. A successful defence would have to close both paths simultaneously
> This case illustrates a failure mode that is becoming increasingly well documented in the literature on AI-assisted formal mathematics: the gap between what a formal proof verifies and what it means. The Lean kernel certifies that a proof term inhabits a given type; it does not certify that the type faithfully encodes the intended mathematical claim. As Tao has emphasised
And afterwards I cross-verified with Pangram 4 which I trust, it marked the preamble/starting stuff as 100% AI-generated.
You're using the wrong names from an older version of their paper and Nielsen's , she's updated to include the new relabels. The proof holds.
That's false. It's not AI generated. It's AI checked. Nielsen has a style that often flags as AI because she uses many EM dashes and has a very rigorous style. Her papers from 2015-2020 also flag as AI generated, before AI was available.
Can you provide a single example of such paper that would show as AI generated on Pangram?
So this is the level of science discourse now? AI really broke people's minds. If it's true or not, it will be eventually proved or not. Name calling really is the best you all can do?
does this show Lean is not bulletproof?
Lean never was bullet proof. Nielsen also provides detailed lean, with correct labels. If you mislabel your labels you can prove the moon is made of cheese in Lean.
Opus 5 says the disproof is wrong.
This attack on Nielsen's paper is crackpottery / academic revenge porn by John Synons. To base an attack on Nielsen on frickin Acerfur is using an undergrad who hasn't passed his first semester yet to take on a PhD student who graduated in physics and math summa cum laude. Nonsense.
A lot of people who know mathematics say Nielsen’s paper is riddled with errors. I regret sharing it here.
> Undergrad who hasn’t passed his first semester yet
Not sure what you’re talking about. According to his wiki bio he’s done two years at Cambridge. He posted Maths questions from the 1B tripos exam, and was smart enough to get an OpenAI internship.
Whereas it seems like the author of this paper has never been hired anywhere by any company or institution — the "Center for Topological Physics" listed seems to exist only as a website.
Nielsen's argument stands: We first disprove the recent OpenAI "disproof" of Connes' rigidity conjecture, then prove the conjecture itself.
Part I shows that the claimed Lean-formalized counterexample is invalid. The crux of the error is that D ⋊ K (a nontrivial semidirect product) is not equivalent to D × K (a trivial direct product), and neither is equivalent to D ×_c K (a cocycle extension with the shiftedCarry cocycle). The formalisation constructs groups of the third type but verifies the ICC property using orbit arguments valid only for the second. In a semidirect product, conjugation acts on the normal factor through the action φ; in a cocycle extension, conjugation acquires five additional terms from the cocycle, which can collapse conjugacy classes and create central elements. We trace the construction through 37,000 lines of published Lean code and identify two independent paths to failure. First, the orbit lemmas underpinning the ICC certificates operate on quotient objects and do not account for the cocycle's contribution to conjugation. Second — and independently dispositive — the zero-cocycle group is a direct product Z^{2n} × Sp(2n, Z) whose centre contains the entire lattice (ruling out ICC) and which surjects onto Z^{2n} (ruling out property (T)). A single failure suffices; this group fails on both counts. The claimed disproof is invalid.
Part II proves the conjecture: every countable discrete ICC group G with Kazhdan's property (T) is W-superrigid, L(G) ≅ L(H) ⟹ G ≅ H. The classical barrier — the absence of Cartan subalgebras in L(G) — is bypassed by lifting to Bernoulli crossed products A_G = L^∞(X) ⋊ G, which possess canonical Cartans. The semidirect structure ⋊ encodes a nontrivial principal G-bundle; this nontriviality is the engine of the proof. We introduce the twisted comultiplication Θ(fu_g) = fu_g ⊗ Φ(u_g), a unital -homomorphism from A_G into A_G ⊗̄ A_H functioning as a connection form between measurable principal bundles. Ioana's classification theorem for Bernoulli actions of property-(T) groups — which classifies arbitrary unital -homomorphisms, with group morphisms as output, not hypothesis — decomposes Θ into morphisms δ₁: G → G and δ₂: G → H. The Bernoulli deformation α_t fixes Θ(L(G)) pointwise, so spectral-gap and absorption arguments apply without hypotheses on the Fourier decomposition of Φ(u_g). Cases (I) and (II) are eliminated by weak convergence and Cartan non-intertwining. A round-trip argument — running the construction symmetrically and using the fact that a surjective -endomorphism of a II₁ factor is an automorphism — forces δ₂ to be a group isomorphism. The conjecture is not disproved; it is proved.
We've banned this account. Please don't post ai-generated comments or engage in combative arguments here. People who have something substantive to contribute do so in the spirit of curious conversation, which is what HN is for. https://news.ycombinator.com/newsguidelines.html