AI Proved What?

Episode 204, October 2026

Only after stretching?

A preprint claims tensor saturation for every even spin group: if an invariant appears after stretching the labels, it was there all along

Covers result 204 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

4:21. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:16The claim
  3. 2:27How the proof goes
  4. 3:39Where it stands

The claim, in plain words

The irreducible representations of a Lie group are labelled by highest weights: points of a lattice inside a cone. Take three of them and ask whether their tensor product contains an invariant, a nonzero vector that the whole group leaves fixed. Stretching all three labels by the same whole number N keeps an invariant that was already there; saturation asks for the converse: if an invariant appears after stretching, was it there all along?

There is a parity test: the three labels must add up to a point of the root lattice. Even then saturation can fail. Our example: for the rotations of 5-dimensional space, three copies of the 5-dimensional representation pass the test, yet no invariant combines three vectors into a number; double the labels and an invariant appears. Knutson and Tao proved saturation for the unitary groups in 1999, and Kapovich and Millson conjectured it for all simply laced groups, those whose roots all have the same length. For the even spin groups it was known only up to Spin(12) (Spin(8) by Kapovich, Kumar and Millson; Spin(10) and Spin(12) by Kiers; Spin(4) and Spin(6) via the unitary case).

Result 204 is one OpenAI preprint, Tensor saturation for even spin groups (46 pages, dated September 24, 2026). Its Theorem 1.1: for Spin(2n), the double cover of the rotation group in 2n dimensions, with n at least 2, and dominant weights λ, μ, ν whose sum lies in the root lattice, an invariant at (Nλ, Nμ, Nν) for some positive whole number N gives one at (λ, μ, ν). The spin representations, with half-integer labels, are included. In Kapovich and Millson’s conjecture, this is the type D part.

What it doesn’t claim

The exceptional groups E6, E7 and E8, the remaining simply laced cases; any formula for how many invariants there are; stretching by fractions, which the paper shows would break the statement (Remark 6.6). Our scans agree with the theorem: among 76,615 small triples for Spin(6) through Spin(16), none fails at the stretches we tried, while the odd rotation and symplectic groups show 226 failures, all at a stretch of two. These ranks are small, and most were already known.

Where it stands

Posted as a preprint
OpenAI, 46 pages, dated September 24, 2026
Peer reviewed
Not yet
Checked in Lean
Not formalized; nothing on this result in the release’s Lean library

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. There is no Lean formalization: nothing about this result is in the release’s Lean library. The paper is not among those OSVerify reviewed, and we found no expert reaction. Our scans and our check of one proposition illustrate the statement; they do not test the proof.

How the proof goes

  1. Forget the integers. An invariant at stretch N gives three skew-symmetric matrices, with eigenvalues set by the stretched labels, that add up to zero (Lemma 2.5). Divide by N, and the stretch disappears.
  2. A real path. From this real solution the paper builds a schedule: start at one label, follow a polygon shaped like the second, reflect in mirror hyperplanes at certain moments, and end at a mirror image of the third (Definition 2.1, Proposition 2.2). Choosing the path of largest area makes the mirror directions independent.
  3. Earn the integers back. The jump at each reflection should be a whole number, but in type D it can be a half. The bad case is a parity defect, exactly two odd pieces of a signed graph (Lemma 3.3); the paper repairs it by sliding along half of one linear relation while keeping the reflections in order (Lemma 3.5, Figure 1, Proposition 3.6 and Section 4, about 12 pages).
  4. Build the invariant. An integral schedule is turned into an actual invariant, one fundamental column at a time (Proposition 5.1). Labels that all end in two or more zeros pass through a smaller spin group at double the stretch (Proposition 6.1), which the paper says introduces no saturation factor.

The numbers in the video

  • Saturation scans (ours), with Freudenthal’s formula and Brauer–Klimyk, spin weights included: type D from Spin(6) to Spin(16), 76,615 small triples passing the parity test, no failures; types B and C, 226 failures among 2,795 such triples, all at a stretch of two.
  • Rotations of 5-space (ours): three copies of the 5-dimensional representation have 0, 1, 0, 1 invariants at stretches 1 to 4.
  • The paper’s Proposition 6.1 checked on 2,093 small cases (ours), no failures.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

A group of rotations acts on vector spaces, and the irreducible ones are labelled by highest weights: points of a lattice inside a cone. Take three of them, and ask a yes-or-no question: does their tensor product contain an invariant, a nonzero vector that every rotation leaves fixed? Now stretch: multiply all three labels by the same whole number N. An invariant at the original labels gives one at every stretch. Saturation asks for the converse: if an invariant appears after stretching, was it there all along? Not always, and not for free. There is a parity test: the three labels must add up to a point of the root lattice. For the rotation group of five-dimensional space, take three copies of its five-dimensional representation. The labels pass the parity test, yet no invariant combines three vectors into a number. Double the labels, and an invariant appears. So for odd rotation groups, saturation can fail. For the unitary groups, Knutson and Tao proved saturation in 1999. Kapovich and Millson conjectured it for all simply laced groups, the ones whose roots all have the same length. For the even spin groups, it was known only up to Spin(12).

1:16The claim

Result 204 is one OpenAI preprint, 46 pages, dated September 24, 2026. It claims saturation for every even spin group, Spin(2n), the double cover of the rotation group in two n dimensions, for n at least two: if three dominant weights add up to a point of the root lattice, and an invariant appears after stretching by some positive whole number, then one is already there at the original labels. The spin representations, with half-integer labels, are included. In Kapovich and Millson’s conjecture, this is the type D part. Not claimed: the exceptional groups E6, E7 and E8, the remaining simply laced cases; any formula for how many invariants there are; or stretching by fractions, which the paper shows would break the statement. Our scans agree. Among more than 76,000 small triples for Spin(6) through Spin(16), none fails at the stretches we tried. In the odd rotation and symplectic groups, our scans find 226 failures, all at a stretch of two. These ranks are small, and most were already known.

2:27How the proof goes

First, forget the integers. An invariant at stretch N gives three skew-symmetric matrices, with eigenvalues set by the stretched labels, that add up to zero. Divide by N, and the stretch disappears. From this real solution the paper builds a path, which it calls a schedule: start at one label, follow a polygon shaped like the second, reflect in mirror hyperplanes at certain moments, and end at a mirror image of the third. Choosing the path of largest area makes the mirror directions independent. Then, earn the integers back. The jump at each reflection should be a whole number, but in type D it can be a half. The paper shows the bad case is a parity defect: exactly two odd pieces of a signed graph. It repairs it by sliding along half of one linear relation, while keeping the reflections in order; about 12 pages go into making that slide work. Finally, an integral schedule is turned into an actual invariant, built one fundamental column at a time. Labels that all end in two or more zeros pass through a smaller spin group at double the stretch, which the paper says introduces no saturation factor.

3:39Where it stands

The preprint is unrefereed and has not been revised. There is no Lean formalization: nothing about this result is in the release’s Lean library. The paper is not among those OSVerify reviewed, and we found no expert reaction. Our scans and our check of one proposition, on 2,093 small cases, illustrate the statement; they do not test the proof. If it holds, the even spin groups join the unitary groups: in type D, an invariant that appears after stretching was there all along. In Kapovich and Millson’s conjecture, only the three exceptional E groups would remain.

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.