Algebra·OpenAI Math·Result 205·Lean formalisation listed
Saxl’s conjecture and universal tensor squares
One of the 372 results in OpenAI's public mathematics catalogue, filed under algebra: 2 preprints, the latest dated 24 September 2026. This page quotes OpenAI's own summary of the claim, links the papers and abstracts, and will embed the animation.
Latest paper
Universal Tensor Squares for Symmetric Groups
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
Proves Saxl's conjecture: the tensor square of every staircase representation contains every irreducible complex representation of the corresponding symmetric group. More generally, every Sn with n ∉ {2,4,9} has an irreducible representation whose tensor square contains all irreducibles. (Lean)
Papers (2)
Universal Tensor Squares for Symmetric Groups
For every positive integer n other than 2, 4, and 9, we prove that some irreducible complex representation of Sn has a tensor square containing every irreducible representation. This resolves the tensor square conjecture for symmetric groups affirmatively.
A Cyclic Polytabloid Proof of Saxl's Conjecture
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.
Status
Preprint. The papers have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Algebra
- 206Finite lattice representation and undecidabilityLean
- 207The ℓ¹-Bass conjecture for all discrete groupsLean
- 208Finite symmetric tensor categories and the Verlinde tower
- 209Integral counterexamples to Gersten’s conjecture
- 210Foulkes' conjecture for sixth powers and quadratic stabilizationLean
- 193Serre’s intersection-multiplicity conjecture