Browse › Algebra › 205 Saxl’s conjecture and universal tensor squares
A Cyclic Polytabloid Proof of Saxl's Conjecture
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 205: Saxl's conjecture and universal tensor squares (lean/docs/205.md, 2026-10-06). The release's Lean development proves $g(\rho_m,\rho_m,\mu)>0$ for all $m\ge1$; the stronger claim that every constituent lies in the cyclic module of one prescribed tensor is stated as not formalized. [family-level]
- OpenAI, Saxl/Main.lean (openai/math, pinned commit adc7f12). The Lean proof file for Theorem 1.1, checked against the comparator statement ComparatorChallenges/Saxl.lean.
- Shuze Chen, The cyclic staircase module inside the tensor square of the staircase Specht module (Prove2Me, 2026-10-18). A Lean definitions bundle extracted from OpenAI's
Saxl/CyclicTensor.leanthat constructs the cyclic module's map into the staircase tensor square and states the stronger cyclic conjecture used by both papers; the page does not supply a proof of that conjecture. [family-level] - Shuze Chen, Content orbits of words, orbit projections and the letter-sum map on word spaces (Prove2Me, 2026-10-18). A definitions bundle extracted from OpenAI's
Saxl/RepeatedProjection.leanwith Lean constructions of the content-orbit projection and letter-sum intertwiner used to detect permutation-module generators in the staircase square. - Keith Adler (with Claude), saxl-lean (GitHub, status dated 2026-10-07). An independent Lean 4/Mathlib project on this paper that re-derives roughly the first half of the argument, proves the staircases (1) through (4,3,2,1) independently, and vendors OpenAI's own complete Lean proof; marked as concluded. [AI-generated per source]
- Keith Adler, mathlib4 PR #44612: conjugacy classes of Perm α are partitions of Nat.card α (mathlib4, opened 2026-10-07, closed unmerged 2026-10-16). A supporting Mathlib contribution from the saxl-lean project, motivated as a counting input for "every irreducible representation of S_n is a Specht module". [AI-generated per source]
Possibly relevant literature (found by the agent, not checked)
- Soong Kyum Lee, Staircase Minimality and a Proof of Saxl's Conjecture (arXiv:2512.15035, Dec 2025). An earlier claimed unconditional proof of the same statement (Theorem 1.1); the arXiv comment says the paper is withdrawn because the claimed proof is not justified in its current form.
- Yutong Chen, Felix Gu, Will Osborne, Spin Representations of Finite Coxeter Groups and Generalisations of Saxl's Conjecture (arXiv:2409.17540, Sep 2024). Proposes generalisations of Saxl's conjecture to Weyl and finite Coxeter groups, giving context for the paper's "History and significance" discussion of the broader covering problem.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 205
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/205.md. The Lean statements have not been checked by people against the paper's claims.
Family 205: Saxl’s conjecture and universal tensor squares
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\notin\{2,4,9\}$ has an irreducible representation whose tensor square contains all irreducibles.
Other papers in this family:
- Universal Tensor Squares for Symmetric Groups · September 24, 2026