Square the staircase: all?
Two preprints claim Saxl’s conjecture, that the square of every staircase representation of a symmetric group contains every irreducible, and its general form for every symmetric group except three small ones, with Lean formalizations of both
Covers result 205 in OpenAI’s catalog: all 2 papers. 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
Shuffle n objects in every possible way: that is the symmetric group. Its irreducible representations are labelled by Young diagrams with n boxes; for six objects there are 11. Multiply one of them by itself, a tensor square, and it breaks into irreducible pieces, counted by Kronecker coefficients. For the staircase with rows 3, 2 and 1, of dimension 16, our computer finds all 11 irreducibles in the square, with multiplicities from 1 to 5.
In 2012 Jan Saxl guessed that this always happens for staircases. Pak, Panova and Vallejo conjectured more broadly that every symmetric group, except for 2, 4 and 9 objects, has some representation whose square contains everything. Those exceptions are real: for 2 objects no diagram is symmetric, and only symmetric diagrams can work; for 4, the only symmetric diagram’s square misses two irreducibles; for 9, the best candidate misses only the 3-by-3 square. As the papers tell it, many families were known, and the staircase’s cube was known to contain everything, but not its square.
Result 205 bundles two OpenAI preprints, both dated September 24, 2026. A Cyclic Polytabloid Proof of Saxl’s Conjecture (17 pages, no computer) claims Saxl’s conjecture: for every staircase, the tensor square contains every irreducible representation. Universal Tensor Squares for Symmetric Groups (37 pages) claims the broader conjecture: for every number of objects except 2, 4 and 9, one fixed diagram whose square contains everything.
What it doesn’t claim
Any formula for the Kronecker coefficients: only that they are positive. Nor is the diagram unique: in our census up to 28 objects, 7 diagrams work for 21 objects and 14 for 28. Away from the staircase sizes, the second paper adds cells symmetrically to a staircase (for odd n from 45 and even n from 66) and uses a computer search up to 64 objects.
Where it stands
- Posted as preprints
- OpenAI, 17 and 37 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Both main statements formalized by OpenAI (docs); not rebuilt by us
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, and neither is among those OSVerify reviewed; we found no expert reaction. Both main statements are formalized in Lean, with machine-checkable statements for Saxl’s conjecture (about 7,500 lines with its imports) and the general theorem (about 217,000 lines), and no unproved steps; we did not rebuild them. An earlier claimed proof of Saxl’s conjecture, posted to arXiv in December 2025, was withdrawn by its author.
How the proof goes
- One vector. The first paper proves something stronger: fill the staircase with positions; in one copy alternate along the rows, in the other along the columns. Their product is a single vector in the square, and every irreducible appears among its shuffles (Theorem 3.1).
- Two halves. Shapes below the staircase in the dominance order come from an explicit map onto a permutation module (Proposition 3.2). For the rest, the paper peels a band of width one or two off the triangle, so that the smaller triangle and the band split apart (Proposition 4.2).
- Two-by-two matrices. The band becomes a product of 2×2 matrices; in one example the product is 12 times a matrix whose corner is zero, and a change of basis turns that corner into 12 (Example 5.4). So every shape with at most four rows appears in the band (Proposition 5.3), and induction, removing at most four horizontal strips, finishes the proof (Lemma 6.1).
- Every degree. The second paper reuses the one-vector statement, adds two tests and a counting argument, partly checked by computer for middle sizes, and exact character arithmetic up to 64 objects.
The numbers in the video
- Exact Kronecker coefficients (ours) from Murnaghan–Nakayama character tables: staircases up to 28 objects contain every irreducible; the staircase (3,2,1) squared has multiplicities 1, 2, 3, 4, 2, 5, 4, 2, 3, 2, 1.
- Census (ours): for every n up to 28, every symmetric diagram tested against every irreducible; none works only at 2, 4 and 9; 1, 2, 3, 7 and 14 diagrams work at 6, 10, 15, 21 and 28 objects.
- Example 5.4 of the first paper reproduced (ours). The Lean line counts are ours.
Read the source
- A Cyclic Polytabloid Proof of Saxl’s Conjecture (PDF), 17 pages.
- Universal Tensor Squares for Symmetric Groups (PDF), 37 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 205.
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
Shuffle n objects in every possible way: that is the symmetric group. Its irreducible representations are labelled by Young diagrams with n boxes; for six objects there are 11. Now take one of them and multiply it by itself, a tensor square. It breaks into irreducible pieces, and the counts are called Kronecker coefficients. For the staircase with rows three, two and one, of dimension 16, our computer finds all 11 irreducibles in the square, with multiplicities from one to five. In 2012, Jan Saxl guessed that this always happens for staircases: the square of the staircase contains every irreducible. Pak, Panova and Vallejo conjectured more broadly that every symmetric group, except for two, four and nine objects, has some representation whose square contains everything. Those exceptions are real. For two objects, no diagram is symmetric, and only symmetric diagrams can work. For four, the only symmetric diagram’s square misses two irreducibles. For nine, the best candidate misses only the three-by-three square. As the papers tell it, many families were known, and the staircase’s cube was known to contain everything, but not its square.
1:17The claim
Result 205 bundles two OpenAI preprints, both dated September 24, 2026. The first, 17 pages, claims Saxl’s conjecture: for every staircase, the tensor square contains every irreducible representation. It uses no computer. The second, 37 pages, claims the broader conjecture: for every number of objects except two, four and nine, there is one fixed diagram whose square contains everything. Not claimed: any formula for the Kronecker coefficients, only that they are positive. Nor is the diagram unique: in our census up to 28 objects, 7 diagrams work for 21 objects, and 14 for 28. Away from the staircase sizes, the second paper adds cells symmetrically to a staircase for large numbers, and uses a computer search up to 64.
2:10How the proof goes
The first paper proves something stronger. Fill the staircase with positions; in one copy, alternate along the rows, in the other along the columns. Their product is a single vector in the square, and every irreducible appears among its shuffles. Shapes below the staircase in the dominance order come from an explicit map onto a permutation module. For the rest, the paper peels a band of width one or two off the triangle, so that the smaller triangle and the band split apart. The band becomes a product of two-by-two matrices. In one example the product comes out as twelve times a matrix whose corner is zero; a change of basis turns that corner into twelve. So every shape with at most four rows appears in the band, and induction, removing at most four horizontal strips, finishes the proof. The second paper reuses this one-vector statement, two tests, and a counting argument, partly checked by computer for middle sizes, and exact character arithmetic up to 64 objects.
3:11Where it stands
Both preprints are unrefereed and have not been revised, and neither is among those OSVerify reviewed; we found no expert reaction. But both main statements are formalized in Lean: about 7,500 lines for Saxl’s conjecture, and about 217,000 for the general theorem, with no unproved steps. We did not rebuild them. An earlier claimed proof, posted in December 2025, was withdrawn. If it holds, every staircase squared contains every irreducible, and every symmetric group, except for two, four and nine objects, has a representation with this property. The Kronecker coefficients themselves still have no known combinatorial rule.
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.