AI Proved What?

Episode 210, October 2026

Does one stack fit in the other?

Two preprints claim Foulkes’ conjecture for sixth powers, and a quadratic bound beyond which it holds for every a

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

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

Chapters

  1. 0:00The question
  2. 1:02The claim
  3. 1:57How the proof goes
  4. 3:04Where it stands

The claim, in plain words

There are two ways to stack symmetric powers: polynomials of degree a in polynomials of degree b, Syma(SymbV), or the other way around, Symb(SymaV). Both carry an action of the general linear group and break into irreducible pieces. In three variables, with a = 2 and b = 3, the first has dimension 55 and the second 56: the same two pieces, plus one extra, the square of the determinant.

In 1950 Foulkes conjectured that when a is at most b, the first always fits inside the second: every irreducible piece appears at least as often on the second side. As the papers tell it, Thrall’s formulas settle a = 2; a = 3, 4 and 5 were proved one case at a time, the last two with computer help, the last published in 2017. A natural map between the two spaces, studied by Howe in 1987, does not always have full rank, so it cannot simply do the job.

Result 210 bundles two OpenAI preprints, both dated September 25, 2026. Quadratic stabilization of the canonical Foulkes–Howe map (7 pages) proves that the natural multiplication map is onto whenever b ≥ a(a − 1), in every dimension, which gives Foulkes’ inequality in that range for every a. Foulkes’ conjecture for the sixth symmetric power (36 pages) finishes the case a = 6: the bound covers b ≥ 30, and computer checks cover 6 ≤ b ≤ 29.

What it doesn’t claim

Foulkes’ conjecture for a ≥ 7 below the bound; that the bound is sharp; or that the natural map itself is the embedding for a = 6. Our own plethysm code agrees with the inequality in 23 small cases, including a = 6 and b = 7, and reproduces three rows of the second paper’s first table.

Where it stands

Posted as preprints
OpenAI, 7 and 36 pages, dated September 25, 2026
Peer reviewed
Not yet
Checked in Lean (partly)
The 7-page theorem (docs); the sixth case only from b = 30; the rest by computer

Last checked October 19, 2026. Neither preprint has been revised since they were added to the repository in its initial commit on October 6, 2026. The 7-page theorem is formalized in Lean (the checked statement): about 5,000 lines with no unproved steps, and the map pinned down exactly; that covers the sixth case only from b = 30. An uncatalogued Lean folder pushes the sixth case down to b = 25 with a stronger bound that appears in neither paper. The degrees in between rest on the computer checks. Neither paper is among those OSVerify reviewed, and we found no expert reaction.

How the proof goes

  1. Forms that vanish on products. The short paper turns surjectivity into a statement about forms: a symmetric form that vanishes on every product of b vectors must be zero, once b ≥ a(a − 1). It moves degree from one variable to another with derivatives, and a single positivity identity (Lemma 2) makes each step reversible. Over the complex numbers a surjection splits, giving the embedding in the other direction.
  2. The sixth power by computer. The sixth-power paper reduces the degrees 6 ≤ b ≤ 29 to a finite list of comparisons between plethysm coefficients: 145,435 base comparisons up to b = 25, then a band of coefficients, all checked by two C++ programs.
  3. A second route. Its own cubic bound covers b ≥ 150, with the programs run that far: about 57 million band coefficients in all. We compiled the first program and ran it once (about 10 minutes); its output matched the authors’ reference byte for byte.

The numbers in the video

  • Three variables, a = 2, b = 3 (ours): 55 = 28 + 27 and 56 = 28 + 27 + 1.
  • Foulkes’ inequality in 23 small cases, including a = 6, b = 7 (ours); rows b = 6, 7, 8 of the sixth-power paper’s Table 1 recomputed; its totals 145,435 and 57,065,668 recounted.
  • The Lean line count is ours.

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

There are two ways to stack symmetric powers. Take polynomials of degree b, then form polynomials of degree a in those; or the other way around, degree a first, then degree b. Both spaces carry an action of the general linear group, and both break into irreducible pieces. In three variables, with a equal to two and b equal to three, the first space has dimension 55 and the second 56: the same two pieces, plus one extra, the square of the determinant. In 1950, Foulkes conjectured that when a is at most b, the first always fits inside the second: every irreducible piece appears at least as often on the second side. As the papers tell it, Thrall’s formulas settle a equal to two; three, four and five were proved one case at a time, the last two with computer help, the last published in 2017. A natural map between the two spaces, which Howe studied in 1987, does not always have full rank, so it cannot simply do the job.

1:02The claim

Result 210 bundles two OpenAI preprints, both dated September 25, 2026. The first, 7 pages, proves that the natural multiplication map is onto whenever b is at least a times a minus one, in every dimension. That gives Foulkes’ inequality in that range for every a. The second, 36 pages, finishes the case a equal to six: the bound covers b from 30 on, and computer checks cover b from 6 to 29. Not claimed: Foulkes’ conjecture for a of seven or more below the bound; that the bound is sharp; or that the natural map itself is the embedding for a equal to six. Our own plethysm code agrees with the inequality in 23 small cases, including a equal to six and b equal to seven, and reproduces three rows of the second paper’s first table.

1:57How the proof goes

The short paper turns surjectivity into a statement about forms. A symmetric form that vanishes on every product of b vectors must be zero, once b is at least a times a minus one. To show it, the paper moves degree from one variable to another with derivatives, and a single positivity identity, its second lemma, makes each step reversible. Over the complex numbers, a surjection splits, and that gives the embedding in the other direction. The sixth-power paper reduces the remaining degrees, b from 6 to 29, to a finite list of comparisons between plethysm coefficients: 145,435 base comparisons up to b = 25, then a band of coefficients, all checked by two C++ programs. It also has a second route: its own cubic bound, from b equal to 150 on, with the programs run that far, about 57 million band coefficients in all. We compiled the first program and ran it once, for 10 minutes; its output matched the authors’ reference byte for byte.

3:04Where it stands

Both preprints are unrefereed and have not been revised. The 7-page theorem is formalized in Lean: about 5,000 lines, with no unproved steps, and the map pinned down exactly; that covers the sixth case only from b = 30. An uncatalogued Lean folder pushes the sixth case down to b = 25 with a stronger bound that appears in neither paper. The degrees in between rest on the computer checks. Neither paper is among those OSVerify reviewed, and we found no expert reaction. If they hold, Foulkes’ inequality holds for every a once b is at least a times a minus one, and the sixth case is settled for every b of at least six.

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.