AI Proved What?

Episode 290, October 2026

The relative case, proved at last?

Two AI preprints re-prove Connes’ bicentralizer conjecture, proved first in September by Houdayer and Marrakchi, and claim the relative version

Covers result 290 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

3:45. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:23The claims
  3. 2:12How the proof goes
  4. 3:08Where it stands

The claim, in plain words

Some von Neumann algebras, those of type III, have no well-behaved trace. But every faithful normal state on them carries its own clock: Tomita–Takesaki theory gives a canonical time evolution, the modular flow, and the part the state treats like a trace is its centralizer. Connes sorted type III factors by the part of this flow’s spectrum shared by every state; with two ratios, 1/2 and 1/3, the gap closes through the logs of 3/2, 9/8 and the Pythagorean comma, the picture of type III1. Around 1980, Connes asked whether, in a type III1 factor, the bicentralizer, everything that commutes, in the limit, with every bounded sequence asymptotically commuting with the state, is just the scalars. Haagerup proved it for the injective factor in 1987. On September 10, 2026, Houdayer and Marrakchi posted a proof of the full conjecture, crediting OpenAI models for key steps.

Result 290 is two OpenAI preprints, 35 pages, dated September 23, 2026. They give what they call an alternative proof of the bicentralizer conjecture for factors with separable predual, and prove what is new: the relative version, formulated by Marrakchi. For an inclusion of von Neumann algebras with separable preduals and a faithful normal conditional expectation, there is an amenable expected subalgebra with the same relative commutant in the continuous core.

What it doesn’t claim

The first proof of Connes’ conjecture, non-separable preduals, or inclusions without a conditional expectation. Houdayer wrote that “OpenAI’s result extends ours by establishing the relative version.”

Where it stands

Posted as preprints
OpenAI, two papers, 35 pages, dated September 23, 2026
Peer reviewed
Not yet
Formalized in Lean
In part: only a technical lemma, neither conjecture (docs)

Last checked October 19, 2026. The preprints have not been revised. In Lean only the bounded recovery lemma is formalized, about 8,000 lines with no unproved steps in our scan, and neither the bicentralizer conjecture nor its relative version is formalized. OSVerify has not reviewed them, and we found no reported doubts.

How the proof goes

  1. A spectral crystal that cannot exist. Both absolute proofs end the same way. Assuming a counterexample, a twist identity forces certain sums of products of spectral coordinates to be multiples of 2π, which only a lattice or an axis can satisfy: the resonance mechanism of Houdayer and Marrakchi.
  2. The relative version. A uniform energy estimate and an unending sequence of random tests, each taking a harmonic-series share of a finite budget, force the needed identity. The second paper reaches the absolute case another way: bounded recovery, the modular spectral recovery of the title, turns spectral vectors back into bounded algebra elements, with bands at most four times wider.

The numbers in the video

  • Ours: a single ratio 1/2 keeps a modular gap of log 2; with ratios 1/2 and 1/3 the gap falls to 0.0136 at 64 sites (the Pythagorean comma) and below 0.0001 at 4,096 sites.
  • Ours: the resonance condition holds for all 2,401 test pairs on a lattice, and fails for 3,660 of 3,721 on a continuous segment.

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The question

Some von Neumann algebras, those of type III, have no well-behaved trace. But every faithful normal state on them carries its own clock: Tomita–Takesaki theory gives a canonical time evolution, the modular flow, and the part the state treats like a trace is its centralizer. Our computer shows the finite version with 4×4 matrices: the flow spins each off-diagonal entry at a speed set by the log of a ratio of eigenvalues, while the diagonal stays frozen. Connes sorted type III factors by the part of this flow’s spectrum shared by every state. With a single ratio, 1/2, the spectrum keeps a fixed gap of log 2 forever. With two ratios, 1/2 and 1/3, our computer finds the gap closing, through the logs of 3/2, 9/8 and the Pythagorean comma, to below 0.0001 at 4,096 sites. That is the picture of type III₁. Around 1980, Connes asked whether, in a type III₁ factor, the bicentralizer, everything that commutes, in the limit, with every bounded sequence asymptotically commuting with the state, is just the scalars. Haagerup proved it for the injective factor in 1987. On September 10, 2026, Houdayer and Marrakchi posted a proof of the full conjecture, crediting OpenAI models for key steps.

1:23The claims

Result 290 is two OpenAI preprints, 35 pages, dated September 23, 2026. They give what they call an alternative proof of the bicentralizer conjecture for factors with separable predual, and prove what is new: the relative version, formulated by Marrakchi. For an inclusion of von Neumann algebras with separable preduals and a faithful normal conditional expectation, there is an amenable expected subalgebra with the same relative commutant in the continuous core. Not claimed: the first proof of Connes’ conjecture, non-separable preduals, or inclusions without a conditional expectation. Houdayer wrote that OpenAI’s result extends theirs by establishing the relative version.

2:12How the proof goes

Both absolute proofs end the same way. Assuming a counterexample, a twist identity forces certain sums of products of spectral coordinates to be multiples of 2π, which only a lattice or an axis can satisfy: the resonance mechanism of Houdayer and Marrakchi. Our computer checks the condition: a lattice passes all 2,401 test pairs, while a continuous segment fails 3,660 of 3,721. For the relative version, a uniform energy estimate and an unending sequence of random tests, each taking a harmonic-series share of a finite budget, force the needed identity. The second paper reaches the absolute case another way: bounded recovery, the modular spectral recovery of the title, turns spectral vectors back into bounded algebra elements, with bands at most four times wider.

3:08Where it stands

The preprints are unrefereed and unchanged since release. In Lean only the bounded recovery lemma is formalized, about 8,000 lines with no unproved steps in our scan, and neither the bicentralizer conjecture nor its relative version is formalized. OSVerify has not reviewed them, and we found no reported doubts. If it holds, Connes’ question is answered twice: by Houdayer and Marrakchi with AI help, and again, for separable preduals, in this release; and the relative version is settled too.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.