Browse › Algebra › 205 Saxl’s conjecture and universal tensor squares
Universal Tensor Squares for Symmetric Groups
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 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.
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 states that it proves Theorem 1.1 for every $n\notin\{2,4,9\}$, including injective intertwining maps for arbitrary finite-dimensional irreducibles, and Saxl's conjecture for every staircase, while excluding the stronger claim about the orbit span of one prescribed tensor. [family-level]
- OpenAI, UniversalSquare/Main.lean (openai/math, pinned commit adc7f12). The Lean proof file for Theorem 1.1, checked against the comparator statement ComparatorChallenges/UniversalTensorSquares.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]
Possibly relevant literature (found by the agent, not checked)
- Mark Sellke, Covering Irrep(S_n) With Tensor Products and Powers (arXiv:2004.05283, accepted in Math. Annalen per arXiv). Studies which tensor products and minimal tensor powers of irreducibles of $S_n$ cover all irreducibles, the setting in which the paper places its tensor-square result against fourth-power and cube coverage.
- Nariel Monteiro, Alexander Stasinski, A tensor square theorem for characters of GL_n(q) (arXiv:2609.17319, 2026-09-15). Constructs an irreducible character of $GL_n(q)$ whose square contains every irreducible character trivial on the centre; related to Corollary 1.2 on unipotent tensor squares of $GL_n(\mathbb F_q)$.
- Soong Kyum Lee, Staircase Minimality and a Proof of Saxl's Conjecture (arXiv:2512.15035, Dec 2025). A withdrawn earlier claimed proof of Saxl's conjecture (the staircase input used here), which also claims staircases are the only Kronecker-universal self-conjugate partitions at triangular degrees.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 205
Independent sites; their content is not reviewed here.
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}
}From OpenAI's README for this paper:
Verification
Use Linux, Bash, Python 3.9 or later, and GNU C++ with C++17 and
unsigned __int128 support. The supplementary comparison also requires the
undefined-behavior sanitizer runtime. Python assertions must be enabled.
Run the complete finite checks from this paper directory in a temporary copy:
set -euo pipefail
verification_work=$(mktemp -d)
cp -R verification "$verification_work/"
cd "$verification_work/verification/code"
g++ -O3 -std=c++17 smallcode_submitted.cpp -o smallcode_submitted
env -u PYTHONOPTIMIZE python3 -B smallcode_verify.py runs 1 3 {5..8} {10..64} \
--seconds 300 --log ../computation/recheck-61-degrees.log
env -u PYTHONOPTIMIZE python3 -B capacity_checks.py intermediate
env -u PYTHONOPTIMIZE python3 -B capacity_checks.py exceptional
Each child of the character driver has a 1536-MiB address-space limit and a
300-second wall limit. Success requires status 0 for every listed degree and
PASS from both capacity checks; a timeout or failed run is not a successful
verification. The excluded degrees 2, 4, and 9 must not be included in this run.
From the same temporary code directory, run the supplementary checks:
env -u PYTHONOPTIMIZE python3 -B capacity_independent.py
g++ -O2 -std=c++17 -fsanitize=undefined \
-fno-sanitize-recover=all smallcode_dump.cpp -o smallcode_dump_ubsan
env -u PYTHONOPTIMIZE python3 -B smallcode_verify.py compare {1..12} \
--log ../computation/recheck-independent.log
env -u PYTHONOPTIMIZE python3 -B -m unittest -v test_smallcode_verify.py
Success requires status 0 for each command, PASS for each independent
comparison, and no unittest failures. Generated binaries and rerun logs remain
in the temporary copy. The build uses the source listings under verification/code/;
the executable verification sources are under verification/code/.
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:
- A Cyclic Polytabloid Proof of Saxl's Conjecture · September 24, 2026