Two languages agree, proved at last?
An AI preprint claims the strongly rational case of the strong-locality conjecture
Covers result 280 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:57. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Two-dimensional conformal field theory describes systems at a critical point, like the Ising magnet at its phase transition. Mathematicians have two rigorous languages for its chiral half. A vertex operator algebra describes the fields through their algebra, an infinite family of modes. A conformal net assigns to every arc of a circle an algebra of bounded observables, and observables on disjoint arcs commute. In 2015, Carpi, Kawahigashi, Longo and Weiner built a bridge: a unitary vertex operator algebra that is strongly local generates a conformal net. They conjectured that every simple unitary one is strongly local, and proved it for affine algebras, the Virasoro algebra and the moonshine module; since then more families have followed, lattices among them.
Result 280 is one OpenAI preprint, 47 pages, dated September 25, 2026. It claims the strongly rational case of the conjecture: every simple unitary vertex operator algebra that is rational, C2-cofinite, of CFT type and self-dual has polynomial energy bounds, is strongly local, and generates a completely rational conformal net. It also claims that every simple module is unitarizable, and that Huang’s modular tensor category is equivalent, as a braided unitary tensor category, to the net’s finite-index sectors. For the Ising model, the spin field has quantum dimension √2 and the net’s μ-index is 4, the sum of the squared dimensions.
What it doesn’t claim
The general conjecture, for algebras that are not strongly rational; the reverse direction, from nets back to vertex operator algebras; or any classification. Many examples were already known. What is new is one proof for the whole class.
Where it stands
- Posted as a preprint
- OpenAI, 47 pages, dated September 25, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- In part: only the first step, energy bounds and strong locality (docs)
Last checked October 19, 2026. The preprint has not been revised. In Lean only the first step is formalized: energy bounds, strong locality and the net, about 29,000 lines; our scan finds no unproved steps, but we did not rebuild it. OSVerify has not reviewed it, and we found no comment from specialists.
How the proof goes
- A speed limit for fields. Fields are unbounded operators, and fields that commute on paper need not give commuting observables. The fix is an energy bound: each mode must be bounded by a power of the energy, with a constant growing only polynomially in the mode number. The paper gets a crude bound and feeds it back into itself, first to a polynomial bound and then to the optimal one, and a criterion of Carpi, Tanimoto and Weiner then gives strong locality.
- Positive modules, matching categories. To give a module a positive inner product, the proof doubles the theory and finds the module, paired with its dual, inside a fusion product of pieces already known to be positive. Gui’s comparison theory then matches fusion and braiding with the net’s Connes fusion and braiding, and, using reconstruction work of Henriques and Tener, the paper shows the net has no extra sectors.
The numbers in the video
- Ours: the Virasoro vacuum module’s inner product through level 20, for central charge from 0.3 to 4/5: no negative norms at 1/2, 7/10 and 4/5; elsewhere a negative-norm state by level 6, 12 or 20.
- Ours: the Ising model’s quantum dimensions 1, 1 and √2, whose squares add to 4.
- Ours: for a free boson, a toy example, creation modes grow like √n on the energy scale.
Read the source
- Strongly Rational Unitary Vertex Operator Algebras and Conformal Nets (PDF), 47 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 280.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Two-dimensional conformal field theory describes systems at a critical point, like the Ising magnet at its phase transition. Mathematicians have two rigorous languages for its chiral half. A vertex operator algebra describes the fields through their algebra, an infinite family of modes. A conformal net assigns to every arc of a circle an algebra of bounded observables, and observables on disjoint arcs commute. In 2015, Carpi, Kawahigashi, Longo and Weiner built a bridge: a unitary vertex operator algebra that is strongly local generates a conformal net. They conjectured that every simple unitary one is strongly local. They proved it for affine algebras, the Virasoro algebra and the moonshine module, and since then more families have followed, lattices among them. Unitarity, a positive inner product, is rare. Our computer checks it on the Virasoro vacuum module: at central charge 1/2, 7/10 and 4/5 no negative-norm state appears through level 20, while at other values from 0.3 to 4/5, one appears by level 6, 12 or 20.
1:11The claims
Result 280 is one OpenAI preprint, 47 pages, dated September 25, 2026. It claims the strongly rational case of the conjecture: every simple unitary vertex operator algebra that is strongly rational, meaning rational, C₂-cofinite, of CFT type and self-dual, has polynomial energy bounds, is strongly local, and generates a completely rational conformal net. It also claims that every simple module is unitarizable, and that the module category, Huang’s modular tensor category, is equivalent as a braided unitary tensor category to the net’s finite-index sectors. So the same numbers appear on both sides. For the Ising model our computer finds the spin field’s quantum dimension, √2, and the net’s μ-index, 4, the sum of the squared dimensions. Not claimed: the general conjecture, for algebras that are not strongly rational; the reverse direction, from nets back to vertex operator algebras; or any classification. Many examples were already known. What is new is one proof for the whole class.
2:20How the proof goes
The hard part is analysis. Fields are unbounded operators, and fields that commute on paper need not give commuting observables. The fix is a speed limit: each mode must be bounded by a power of the energy, with a constant growing only polynomially in the mode number. For a free boson, a toy example, our computer finds the creation modes grow like √n. The paper gets a crude bound and feeds it back into itself, first to a polynomial bound and then to the optimal one, and a criterion of Carpi, Tanimoto and Weiner then gives strong locality. Next, every module needs a positive inner product. To reach one that has none yet, the proof doubles the theory and finds the module, paired with its dual, inside a fusion product of pieces already known to be positive. Gui’s comparison theory then matches fusion and braiding with the net’s Connes fusion and braiding, and, using reconstruction work of Henriques and Tener, the paper shows the net has no extra sectors.
3:24Where it stands
The preprint is unrefereed and unchanged since release. In Lean only the first step is formalized: energy bounds, strong locality and the net, about 29,000 lines; our scan finds no unproved steps, but we did not rebuild it. OSVerify has not reviewed it, and we found no comment from specialists. If it holds, then every strongly rational unitary theory gives a conformal net with exactly the same modules, fusion and braiding.
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.