Algebra · Result 205

Saxl’s conjecture and universal tensor squares

2 papersLean

Proves Saxl's conjecture: the tensor square of every staircase representation contains every irreducible complex representation of the corresponding symmetric group. More generally, every S_n with \(n\notin\{2,4,9\}\) has an irreducible representation whose tensor square contains all irreducibles.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Universal Tensor Squares for Symmetric Groups

OpenAI · September 24, 2026

For every positive integer n other than 2, 4, and 9, we prove that some irreducible complex representation of S_n has a tensor square containing every irreducible representation. This resolves the tensor square conjecture for symmetric groups affirmatively.

Read PDF Download Source

Cite

@misc{OAI:Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026,
  author = {{OpenAI}},
  title = {{Universal Tensor Squares for Symmetric Groups}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf}{OAI:Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026}},
  year = {2026}
}

A Cyclic Polytabloid Proof of Saxl's Conjecture

OpenAI · September 24, 2026

For every staircase partition, we prove that the tensor square of the corresponding irreducible complex representation of the symmetric group contains every irreducible representation of that group. This proves Saxl's conjecture.

Read PDF Download Source

Cite

@misc{OAI:A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026,
  author = {{OpenAI}},
  title = {{A Cyclic Polytabloid Proof of Saxl's Conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf}{OAI:A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves the universal tensor-square conjecture for symmetric groups in the stated range. For every positive integer \(n\notin\{2,4,9\}\), it constructs an irreducible complex representation of \(S_n\) whose tensor square contains every irreducible complex representation of \(S_n\). Equivalently, all corresponding Kronecker coefficients are positive. The statement also supplies injective intertwining maps for arbitrary finite-dimensional irreducible representations.

Saxl's conjecture asserts that the tensor square of each staircase Specht module contains every irreducible representation of the corresponding symmetric group. The formalization establishes this for every \(m\ge1\): if \(\rho_m=(m,m-1,\ldots,1)\), then \(g(\rho_m,\rho_m,\mu)>0\) for every partition \(\mu\) of \(m(m+1)/2\).

The stronger claim that every constituent appears in the orbit span of one prescribed tensor is not included.

Comparator links

Result	Comparator statement
Universal irreducible tensor squares for symmetric groups	UniversalTensorSquares.lean
Saxl's conjecture	Saxl.lean

Scope note on GitHub →