Representation Theory

Motivation: Saxl's conjecture on the staircase tensor square

The irreducible complex representations of the symmetric group $S_n$ are the Specht modules $S^\lambda$, indexed by partitions $\lambda\vdash n$. How a tensor product $S^\alpha\otimes S^\beta$ (with diagonal action) decomposes is recorded by the Kronecker coefficients

$$g(\alpha,\beta,\lambda)=\dim\operatorname{Hom}_{S_n}\!\big(S^\lambda,\,S^\alpha\otimes S^\beta\big),$$

for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase $\rho_m=(m,m-1,\dots,1)$, a partition of $N_m=m(m+1)/2$, has a tensor square containing every irreducible representation of $S_{N_m}$.

Timeline

• 2012 — Saxl proposes the conjecture at the UCLA Combinatorics Seminar (20 March 2012), as recorded by Pak, Panova and Vallejo.
• 2010 — Brown, van Willigenburg and Zabrocki show that $S^{(m,m-1)}\otimes S^{(m,m-1)}$ is the multiplicity-free sum of all irreducibles with at most four rows (BWZ 2010, Cor. 4.1).
• 2013 — Heide, Saxl, Tiep and Zalesski prove that the Steinberg square of most finite simple groups of Lie type contains every irreducible, a motivating precedent (HSTZ 2013, Thm 1.2).
• 2015 — Ikenmeyer proves positivity for all $\lambda$ comparable with $\rho_m$ in dominance order, and all hooks (Ikenmeyer 2015).
• 2016 — Pak, Panova and Vallejo formulate the conjecture in print, give a character-nonvanishing criterion, and handle hooks and two-row shapes for large $m$ (PPV 2016).
• 2017 — Luo and Sellke: almost every partition occurs (uniform and Plancherel measures) (Luo–Sellke 2017).
• 2018–2021 — Bessenrodt: double hooks (2018); Bessenrodt, Bowman and Sutton: all 2-height-zero constituents and framed staircases (2021); Li: triple hooks (2021).
• 2023 — Harman and Ryba: the staircase tensor cube contains everything (Harman–Ryba 2023).
• 2025 — Letellier and Nam prove the staircase-square statement for unipotent characters of $\mathrm{GL}_n(q)$, a different character theory (Letellier–Nam 2025).
• 2026 — An OpenAI preprint, A Cyclic Polytabloid Proof of Saxl's Conjecture (OpenAI Math Release, September 24, 2026), claims a proof of the full conjecture. It has not been peer reviewed and the theorem is not formally verified.

Setting

A partition is a Mathlib YoungDiagram. The Lean development builds $S^\lambda$ concretely: for a tableau $t$ (a bijection between $\{0,\dots,n-1\}$ and the cells), the polytabloid $e_t$ is the signed sum over the column group of $t$ of the permuted indicator of the row word of $t$, inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$; Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The coefficient kronecker a b t is the complex dimension of the space of $S_n$-intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells $(i,j)$ with $i+j<m$, i.e. $\rho_m$.

Formalization targets

Goal: Saxl's conjecture

For every integer $m\ge1$ and every partition $\lambda\vdash N_m$,

$$g(\rho_m,\rho_m,\lambda)>0 ,$$

equivalently $S^{\rho_m}\otimes S^{\rho_m}$ contains every irreducible representation of $S_{N_m}$. This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram $\mu$ with as many cells as staircase m). The goal is published on the platform with status Open.

Significance

The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every $S^\lambda$ already occurs in the submodule $W_m$ generated by one explicit tensor $v_{R_m}\otimes v_{C_m}$ of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every $n\notin\{2,4,9\}$, an irreducible representation of $S_n$ whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).

Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of $S_n$.

Difficulty

Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all $\lambda$) or higher powers (cube, fourth power) leave exceptional constituents. An induction on $m$ must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.

Formalization scope

• staircase m has cells $\{(i,j): i+j<m\}$, with $m(m+1)/2$ cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.
• kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map $S^\lambda\to S^{\rho_m}\otimes S^{\rho_m}$ exists.
• The case $m\ge1$ matches the source; $m=0$ is excluded.
• Needed infrastructure: Specht modules and polytabloid bases, Young's rule and dominance, sign twists, induction and restriction, Littlewood–Richardson branching. The definitions are shared verbatim with the companion universal-tensor-square mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• A. A. H. Brown, S. van Willigenburg and M. Zabrocki, Expressions for Catalan Kronecker products, Pacific J. Math. 248 (2010), 31–48. https://doi.org/10.2140/pjm.2010.248.31
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• C. Bessenrodt, C. Bowman and L. Sutton, Kronecker positivity and 2-modular representation theory, Trans. Amer. Math. Soc. Ser. B 8 (2021), 1024–1055. https://doi.org/10.1090/btran/70
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier and G. Nam, The Saxl conjecture and the tensor square of unipotent characters of GL_n(q), Algebr. Comb. 8 (2025), 1119–1140. https://doi.org/10.5802/alco.434
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf

Motivation

The real Clifford algebra $\mathrm{Cl}(6,0)$ is the smallest Euclidean Clifford algebra whose full structure carries a nontrivial multiplicity-eight representation-theoretic decomposition, and it has become a recurring object in programs that build internal gauge and family structure from Clifford generators rather than imposing it by hand. Within such programs, the single most basic representation-theoretic question one can ask about the algebra is: how does a distinguished $\mathfrak{su}(2)$ subalgebra, acting by the adjoint action, decompose the odd part of the algebra as a representation?

This mission answers that question exactly, for the specific triple of bivectors built on the index set $\{0,2,5\}$. The computation was carried out structurally (by splitting active indices from spectator indices) in the LeanProofs research program in 2026 and recorded with exact multiplicities; no machine-checked proof exists yet. The purpose here is to close that gap: the result is finite-dimensional linear algebra, completely within reach of a Lean 4 + Mathlib development, and every constant in it is explicit.

Setting

Fix $\mathbb{R}^6$ with its standard inner product and the associated quadratic form $Q_{60} = \mathrm{diag}(1,1,1,1,1,1)$, and let $\mathrm{Cl}(6,0) = \mathrm{CliffordAlgebra}(Q_{60})$ be the real Clifford algebra generated by symbols $e_0,\dots,e_5$ with

$$e_i^2 = 1, \qquad e_i e_j = -e_j e_i \ \ (i \neq j).$$

The algebra is $\mathbb{Z}$-graded in the usual sense: it is the direct sum of its grade-$k$ subspaces, spanned by products of $k$ distinct generators, of dimension $\binom{6}{k}$. The odd sector is the linear span of the odd grades,

$$\mathrm{Cl}^-(6,0) \;=\; \mathrm{grade}_1 \oplus \mathrm{grade}_3 \oplus \mathrm{grade}_5, \qquad \dim_{\mathbb{R}} \mathrm{Cl}^-(6,0) = 6 + 20 + 6 = 32.$$

On it, register three bivectors and their halved adjoint actions:

$$E_1 = e_0 e_2, \quad E_2 = e_2 e_5, \quad E_3 = e_0 e_5, \qquad T_i = \tfrac{1}{2}\,\mathrm{ad}_{E_i},$$

where $\mathrm{ad}_{X}(Y) = XY - YX$. The triple satisfies the $\mathfrak{su}(2)$ relations $[E_1,E_2]=2E_3$ and cyclic permutations, so the $T_i$ generate a copy of $\mathfrak{su}(2)$ with $[T_1,T_2]=T_3$ cyclically. The associated quadratic Casimir is the endomorphism

$$C \;=\; -(T_1^2 + T_2^2 + T_3^2).$$

Because each $E_i$ is even, every $T_i$ preserves the odd sector, and so does $C$.

Formalization targets

Goal — the Casimir spectrum with exact multiplicities

$$C\big|_{\mathrm{Cl}^-(6,0)} \ \text{has eigenvalue } 2 \text{ with multiplicity } 24 \ \text{and eigenvalue } 0 \text{ with multiplicity } 8,$$

the two eigenspaces spanning the whole odd sector. Equivalently, as a representation of the generated $\mathrm{Spin}(3) \cong \mathrm{SU}(2)$,

$$\mathrm{Cl}^-(6,0) \;\cong\; 8\,V_{j=1} \;\oplus\; 8\,V_{j=0},$$

eight copies of the spin-1 module and eight copies of the trivial module. The goal deliberately asserts only the eigenspace dimensions and their spanning property — the decomposition shape — not any particular basis or pairing.

Stronger — the Cartan weight decomposition

$$T_3\text{-weights on } \mathrm{Cl}^-(6,0): \quad 0 \ \text{(multiplicity } 16\text{)}, \qquad +1 \ \text{and} \ -1 \ \text{(multiplicity } 8 \text{ each)},$$

the three weight spaces spanning the sector. This refines the goal: each $j=1$ copy contributes weights $-1,0,+1$ and each $j=0$ copy contributes weight $0$.

Significance

The result itself. The spectrum pins down exactly how an $\mathfrak{su}(2)$ acting from inside the algebra sees the odd sector: not irreducibly, but as a clean $8 \oplus 8$ multiplicity split between spin-1 and spin-0. In the LeanProofs program this decomposition is load-bearing for everything downstream that distinguishes "active" indices from "spectator" indices — the multiplicity $8$ is the number of spectator degrees of freedom, and its appearance in the spectrum is what makes the split structural rather than coincidental. The weight decomposition further identifies the Cartan grading and is the natural first test case for any technology that must eventually handle larger Clifford algebras or other subalgebras.

Formalizing it. The computation is proved (structurally, by hand, in the research record) but not machine-checked. Everything needed lives in Mathlib: CliffordAlgebra, its $\mathbb{Z}_2$ grading CliffordAlgebra.evenOdd, Submodule, LinearMap, Module.finrank. What the mission produces is a fully verified finite spectral computation inside Clifford algebra — a reusable certificate that the platform's Clifford and grading infrastructure supports exact representation-theoretic bookkeeping, not just algebraic identities.

Difficulty

The obstruction is bookkeeping, not ideas. The natural attack — split indices into active $\{0,2,5\}$ and spectator $\{1,3,4\}$, decompose $\mathrm{Cl}(\text{active}) \otimes \mathrm{Cl}(\text{spectator})$ as a tensor product of graded pieces, and read off the $8 = 2^3$ multiplicity from the spectator sector — requires transferring the $\mathfrak{su}(2)$ action across such a tensor decomposition, which Mathlib does not provide ready-made for Clifford algebras. A purely computational route (fix the 64-element blade basis, build the $32 \times 32$ matrices of the $T_i$ explicitly, compute kernels) is straightforwardly correct but laborious; making it readable is the real work. The statement is stated through arbitrary endomorphisms bound pointwise to the halved adjoint actions precisely so that solvers may choose either route.

Formalization scope

The mission commits to: the quadratic form Q60 as QuadraticMap.weightedSumSquares ℝ (fun _ : Fin 6 => 1); generators e6 i = CliffordAlgebra.ι Q60 (Pi.single i 1); the odd sector as the Mathlib-native CliffordAlgebra.evenOdd Q60 1; and the registered triple as products of two generators. All theorems quantify over endomorphism witnesses bound pointwise to $\tfrac12\,\mathrm{ad}_{E_i}$, so no particular matrix realization is privileged. Spectra are stated as eigenspace decompositions with exact Module.finrank multiplicities — never as pointwise eigenvalue claims, which would be false for mixed vectors. No trivializing formalization exists: the multiplicities are hard constants, and the dimension gate (32) rules out statements about degenerate sector choices. The definition file is reusable for any future mission on $\mathrm{Cl}(6,0)$; the su(2) relations and dimension gate are self-contained milestones. Contributions of either a structural (active/spectator split) or computational (explicit blade basis) proof are equally welcome.

Selected references

• Lawson & Michelsohn, Spin Geometry, Princeton University Press, 1989 (Clifford algebra grading and structure).
• MonumentalSystems, LeanProofs research record #2561 (2026): exact full-sector SU(2) decomposition of $\mathrm{Cl}^-(6,0)$ with multiplicities, https://github.com/MonumentalSystems/LeanProofs
• Mathlib, Mathlib.LinearAlgebra.CliffordAlgebra.Grading (the evenOdd grading used as the odd sector).

Motivation

Waldspurger's non-standard fundamental lemma is an identity between stable orbital integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even isogenous as algebraic groups, but whose root data become identified after tensoring with $\mathbb{Q}$. The basic example is the pair $(\mathrm{Sp}_{2n}, \mathrm{SO}_{2n+1})$, whose root systems $C_n$ and $B_n$ are exchanged by Langlands duality; the identity is what allows the twisted fundamental lemma to be deduced from the ordinary one. Waldspurger formulated the conjecture in L'endoscopie tordue n'est pas si tordue (2008); it is Theorem 1.12.7 of Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), proved there in equal characteristic by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.

Before any of that geometry can start, the two sides have to be compared: one needs a single Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving both groups at once. Producing that comparison is a self-contained piece of linear algebra over the root data, carried out in Ngo's §1.12, and it is what this mission asks for.

Setting

Let $G_1$ and $G_2$ be split reductive groups over a field, pinned, with maximal tori $T_1$ and $T_2$. Each is determined by its root datum $(X^*(T_i), X_*(T_i), \Phi_i, \Phi_i^\vee, \Delta_i)$, where $\Phi_i$ is the set of roots, $\Phi_i^\vee$ the set of coroots and $\Delta_i$ the set of simple roots singled out by the pinning.

An isogeny of root data between $G_1$ and $G_2$ (Ngo, Definition 1.12.1) is a pair of isomorphisms of $\mathbb{Q}$-vector spaces

$$\psi^* : X^*(T_2)\otimes\mathbb{Q} \longrightarrow X^*(T_1)\otimes\mathbb{Q}, \qquad \psi_* : X_*(T_1)\otimes\mathbb{Q} \longrightarrow X_*(T_2)\otimes\mathbb{Q}$$

which are transposes of one another, such that $\psi^*$ carries the set of lines $\mathbb{Q}\alpha_2$ ($\alpha_2 \in \Phi_2$) bijectively onto the set of lines $\mathbb{Q}\alpha_1$ ($\alpha_1\in\Phi_1$), matching lines of simple roots with lines of simple roots, and such that $\psi_*$ has the same property for the lines spanned by coroots. Two semisimple groups with the same adjoint group are isogenous in this sense; so are a group and its Langlands dual, the interesting cases being $B_n \leftrightarrow C_n$, $F_4$ and $G_2$, where a short root $\alpha$ is sent to $\check\alpha$ and a long root to $n\check\alpha$ with $n = |\alpha_{\mathrm{long}}|^2/|\alpha_{\mathrm{short}}|^2$. Groups obtained by twisting a pair of isogenous pinned groups by a common torsor are called paired.

A prime $p$ is good with respect to $\psi^*$ when it divides neither of the indices

$$\bigl|X_*(T_1)/(X_*(T_1)\cap X_*(T_2))\bigr| \quad\text{and}\quad \bigl|X_*(T_2)/(X_*(T_1)\cap X_*(T_2))\bigr|,$$

the two lattices being compared inside the single $\mathbb{Q}$-vector space identified by $\psi_*$.

Formalization targets

Goal (1.12.4 and 1.12.6): the Weyl groups are identified compatibly

$$\psi_* \, w \, \psi_*^{-1} \in W_2 \quad \text{for all } w \in W_1, \qquad\text{and conversely,}$$

i.e. conjugation by $\psi_*$ carries the Weyl group $W_1$ acting on $X_*(T_1)\otimes\mathbb{Q}$ onto the Weyl group $W_2$ acting on $X_*(T_2)\otimes\mathbb{Q}$. Ngo's reason is that the reflection attached to a root depends only on the line through that root, so the bijection of root lines transports reflections to reflections. This equivariance is what makes the induced isomorphism $\mathfrak{t}_1 \to \mathfrak{t}_2$ descend to an isomorphism $\nu : \mathfrak{c}_{G_1} \to \mathfrak{c}_{G_2}$ of the spaces of characteristic polynomials, which is Lemme 1.12.6 and which is what allows two points $a_1$ and $a_2$ with $\nu(a_1) = a_2$ to be compared at all.

Milestones

Two steps lead there: the reflection computation that makes a matched pair of root lines give a matched pair of reflections, and the integral statement behind Ngo's good-characteristic hypothesis — that when the two indices above are invertible in the base ring, the two lattices become identified after base change.

Significance

Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over $O_v = k[[\varpi]]$ with residue characteristic exceeding twice the Coxeter numbers, and for points $a_1$ and $a_2$ corresponding under $\nu$, the stable orbital integrals of the characteristic functions of $\mathfrak{g}_1(O_v)$ and $\mathfrak{g}_2(O_v)$ agree. Waldspurger showed that this identity, together with the ordinary fundamental lemma, implies the twisted fundamental lemma. None of the objects in that statement — reductive group schemes over a discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the isomorphism $\nu$ the two sides of Theorem 1.12.7 cannot even be matched up.

Beyond this paper, the notion of an isogeny of root data and the good-characteristic base change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands duality for split groups, and neither is currently available.

Difficulty

The reflection step looks like a one-line computation and is one — but only once the two proportionality constants are known to agree. If $\psi^*(\alpha_2) = c\,\alpha_1$ and $\psi_*(\alpha_1^\vee) = c'\,\alpha_2^\vee$, the conjugate of $s_{\alpha_1}$ is $s_{\alpha_2}$ exactly when $c = c'$, and that is forced by transposition together with $\langle\alpha,\alpha^\vee\rangle = 2$. The genuine difficulty in the goal is different: the definition only says that $\psi^*$ and $\psi_*$ permute lines, so one has to show that the bijection induced on root lines and the bijection induced on coroot lines are the same bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.

The lattice milestone has its own trap: the quotient $\Lambda_1/(\Lambda_1\cap\Lambda_2)$ must be shown to have vanishing $\mathrm{Tor}$ after base change, not merely to vanish, or the inclusion becomes only surjective.

Formalization scope

Root data are modelled by Mathlib's RootPairing ι ℚ M N, with $M$ the character space, $N$ the cocharacter space, and rational coefficients throughout, so that "tensoring with $\mathbb{Q}$" is built into the ambient objects rather than performed explicitly. A choice of simple roots is recorded as a subset of the index type rather than as a RootPairing.Base; nothing in the statements depends on that subset beyond its role in the definition of an isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space generated by the coreflections, which is the form in which it acts on the Cartan.

The goal is stated as a two-sided intertwining property rather than as an equality of subgroups: every element of $W_1$ is intertwined by $\psi_*$ with some element of $W_2$ and conversely. This avoids introducing a conjugation homomorphism, and it is the form in which the statement is used. Both root pairings in the goal are required to be finite, reduced root systems, matching Ngo's hypothesis that $G_1$ and $G_2$ are reductive groups.

The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility in the base ring of the two indices, each expressed as the cardinality of an explicit quotient group; the conclusion is the bijectivity of the map induced on the tensor product by the inclusion of the intersection. If a quotient were infinite its cardinality is reported as $0$, and invertibility of $0$ then forces the base ring to be trivial, so no false statement hides in that corner.

No statement here is vacuous: any pair consisting of a root system and itself, with $\psi^*$ and $\psi_*$ the identity, satisfies every hypothesis, and the pair $(B_n, C_n)$ gives the intended non-trivial instances.

Selected references

• Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
• J.-L. Waldspurger, L'endoscopie tordue n'est pas si tordue, Mem. Amer. Math. Soc. 908 (2008). https://doi.org/10.1090/memo/0908
• J.-L. Waldspurger, Le lemme fondamental implique le transfert, Compositio Math. 105 (1997), 153-236. https://doi.org/10.1023/A:1000103112268
• T. A. Springer, Reductive groups, in Automorphic Forms, Representations and L-functions, Proc. Sympos. Pure Math. 33 (1979), 3-27. https://doi.org/10.1090/pspum/033.1

Motivation

An expander is a sparse graph in which every set of vertices has many neighbours outside itself. Expanders are the building blocks of superconcentrators (sparse directed graphs that route any $r$ inputs to any $r$ outputs along vertex-disjoint paths), of sorting and switching networks, and of many constructions in complexity theory and coding; the survey of Hoory, Linial and Wigderson (Bull. AMS 2006) describes these uses. Random regular graphs are expanders with high probability, but applications need explicit families with fixed degree and a uniform expansion constant.

Alon and Milman (J. Combin. Theory Ser. B 38 (1985)) replace combinatorial expansion by a spectral quantity, the second-smallest eigenvalue $\lambda_1$ of the matrix $Q = D - A$ of a graph, which Fiedler called the algebraic connectivity (Czech. Math. J. 1973). Their Theorem 4.3 shows that a regular graph with $\lambda_1$ bounded away from $0$ yields an expander. This mission formalizes their Section 4 source of such graphs: Cayley graphs of the finite quotients of a group with Kazhdan's property (T).

Timeline:

• 1967: Kazhdan introduces property (T) and proves that $SL(n,\mathbb{Z})$, $n \ge 3$, has it (Funct. Anal. Appl. 1 (1967)).
• 1973: Margulis uses property (T) to give the first explicit expander family (Probl. Inf. Transm. 9 (1973)).
• 1981: Gabber and Galil give a variant of Margulis' construction with an explicit expansion constant, proved by Fourier analysis (J. Comput. Syst. Sci. 22 (1981)).
• 1985: Alon and Milman state the construction in terms of $\lambda_1$ (Lemma 4.8, Theorem 4.9) and link it to the concentration property of Section 2 of their paper.

Setting

Let $T$ be a finite group. A finite multigraph on $T$ is a symmetric matrix $M = (M_{w,u})$ of nonnegative integers, $M_{w,u}$ being the number of edges joining $w$ and $u$ (diagonal entries count loops). It is $k$-regular if every row sums to $k$. Its matrix is $Q = \operatorname{diag}(d(v)) - M$ with $d(v) = \sum_u M_{v,u}$, a real symmetric positive semidefinite matrix. Its eigenvalues, repeated according to multiplicity, are $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{|T|-1}$, and $\lambda_1(G)$ denotes the second of them.

Let $H$ be a group, $S \subseteq H$ a finite set with $S = S^{-1}$, and $\phi : H \to T$ a homomorphism onto $T$. The Cayley multigraph $G(T, \phi(S))$ joins $w$ and $u$ by as many edges as there are $s \in S$ with $w u^{-1} = \phi(s)$. It is $|S|$-regular, and its matrix is $Q = |S| \cdot I - \sum_{s\in S} \pi(\phi(s))$, where $\pi(t)$ is the permutation matrix of the left regular representation, $(\pi(t))_{w,u} = 1$ iff $w u^{-1} = t$.

An $(n,k,\varepsilon)$-enlarger (Definition 4.1) is a $k$-regular graph on $n$ vertices with $\lambda_1 \ge \varepsilon$.

A unitary representation $\pi$ of $H$ in a complex Hilbert space $V$ is essentially nontrivial (Definition 4.5) if no nonzero vector is fixed by every $\pi(h)$. A discrete group $H$ has property (T) (Definition 4.6) if there are $\varepsilon > 0$ and a finite $K \subseteq H$ such that for every essentially nontrivial unitary representation $\pi$ and every unit vector $y$ some $h \in K$ satisfies $|(\pi(h)y, y)| < 1 - \varepsilon$.

Formalization targets

Goal: Theorem 4.9

Let $H$ have property (T), let $S$ be a finite generating set of $H$ with $S = S^{-1}$, and let $\phi_i : H \to T_i$ be surjective homomorphisms onto finite groups with $|T_i| \to \infty$. Then there is one $\varepsilon > 0$ with

$$G(T_i, \phi_i(S)) \text{ is a } (|T_i|,\ |S|,\ \varepsilon)\text{-enlarger for every } i \text{ with } |T_i| \ge 2 .$$

The constant is unspecified: the theorem asserts uniformity in $i$, not a value.

Milestones, in the order the paper's argument uses them

1. Lemma 4.7. For any generating set $S$ of a property (T) group there is $\varepsilon > 0$ such that every essentially nontrivial unitary representation and every unit vector $y$ admit $s \in S$ with $|(\pi(s)y,y)| < 1-\varepsilon$.
2. Proof of Lemma 4.8, essential nontriviality. For $\phi$ onto $T$, every nonzero vector of $W = \{v : \sum_t v_t = 0\}$ is moved by some $\pi(\phi(h))$.
3. Proof of Lemma 4.8, Rayleigh's principle. For the Cayley multigraph, $\min\{(Qy,y) : y \in W,\ \|y\| = 1\} = \lambda_1(G)$.
4. Lemma 4.8. With $H$, $S$ and $\varepsilon$ as in Lemma 4.7, $S$ finite and $S = S^{-1}$, and $\phi$ onto a finite group $T$, the Cayley graph $G(T,\phi(S))$ is a $(|T|, |S|, \varepsilon)$-enlarger.

Significance

Theorem 4.9 turns an analytic property of one infinite group into a uniform spectral bound for infinitely many finite graphs of fixed degree. With Theorem 4.3 of the paper it produces explicit families of linear expanders, hence of linear superconcentrators; for $H = SL(n,\mathbb{Z})$, $n \ge 3$, and its reductions modulo $i$ the paper obtains infinitely many explicit families of $(n, 4, \varepsilon)$-enlargers. The same mechanism underlies later work on expanders from groups, surveyed in Lubotzky's monograph (Birkhäuser 1994).

The result is proved in the paper, modulo Lemma 4.7, which the paper refers to Margulis for. The formalization adds a checked account of every step, including Lemma 4.7 itself. At the pinned Mathlib revision there is no notion of property (T), of Kazhdan constants, or of the algebraic connectivity of a multigraph, and no machine-checked version of Theorem 4.9 is known on this platform.

Difficulty

The combinatorial and linear-algebra steps are routine; the substance is in two places. First, Lemma 4.7: Definition 4.6 supplies a constant for one finite set $K$, nothing in the definition relates $K$ to a given generating set $S$, the paper gives no proof, and the standard references state the textbook form $\|\pi(h)y - y\| \ge \varepsilon$ rather than the paper's absolute-value form $|(\pi(h)y,y)| < 1-\varepsilon$. Second, the uniformity: a spectral gap for each fixed quotient is easy, since a connected graph has $\lambda_1 > 0$, but a bound that does not decay as $|T_i| \to \infty$ is exactly what cannot come from any finite computation and must come from property (T) through Lemma 4.8. The Rayleigh quotient of milestone 3 is taken over real vectors, while Lemma 4.7 is stated for complex Hilbert spaces.

Formalization scope

Groups are Lean types with a Group instance; the finite groups $T$ carry Fintype and DecidableEq. Graphs are multigraphs given by symmetric matrices Matrix T T ℕ, with loops allowed. This matters: when $\phi$ identifies two generators or sends one to the identity, the degree is still $|S|$, and a loop contributes $0$ to $Q$. Mathlib's SimpleGraph Cayley graph forgets these multiplicities and is not used. $\lambda_1$ is the second-smallest eigenvalue with multiplicity of the real symmetric matrix $Q$ (via Matrix.IsHermitian.eigenvalues₀). It is defined spectrally, as in the paper, and not as a Rayleigh minimum. It is only meaningful for $|T| \ge 2$, and the goal excludes trivial quotients explicitly. Unitary representations are homomorphisms into the unitary group of bounded operators on a complex Hilbert space in universe Type. Compact subsets of a discrete group are finite sets.

A trivializing formalization is ruled out. Property (T) is not replaced by the hypothesis that the regular representations of the quotients have no almost-invariant vectors, which would make Theorem 4.9 a restatement of its hypothesis. And $\lambda_1$ is not defined as the minimum of $(Qy,y)$ over zero-sum unit vectors, which would make milestone 3 true by definition.

A complete development needs basic Kazhdan-constant manipulations, Courant–Fischer for real symmetric matrices, and the regular representation of a finite group as a unitary representation. The regularity of Cayley multigraphs and the identity $Q = |S| I - \sum_s \pi(\phi(s))$ are short. The spectral and representation-theoretic lemmas are reusable beyond this mission. Contributions of intermediate lemmas, such as the variational characterization of eigenvalues₀ or the invariance of the zero-sum subspace, are welcome.

Selected references

• N. Alon, V. D. Milman, λ1, Isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• D. A. Kazhdan, Connection of the dual space of a group with the structure of its closed subgroups, Funct. Anal. Appl. 1 (1967) 63–65. https://doi.org/10.1007/BF01075866
• G. A. Margulis, Explicit constructions of concentrators, Probl. Inf. Transm. 9 (1973) 325–332. http://mi.mathnet.ru/ppi1162
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Comput. Syst. Sci. 22 (1981) 407–420. https://doi.org/10.1016/0022-0000(81)90040-4
• M. Fiedler, Algebraic connectivity of graphs, Czech. Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• A. Lubotzky, Discrete Groups, Expanding Graphs and Invariant Measures, Birkhäuser, 1994. https://doi.org/10.1007/978-3-0346-0332-4
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Cambridge University Press, 2008. https://doi.org/10.1017/CBO9780511542749
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

How many ways can a closed orientable surface of genus $g$ be "coloured" by a finite group $G$? Precisely: how many group homomorphisms $\pi_1(\Sigma_g)\to G$ are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group $G$. That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of $G$ alone. It is known as Mednykh's formula.

Timeline. Frobenius (1896) counted pairs with a prescribed commutator, $\#\{(a,b):[a,b]=z\}$, in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of $\pi_1(\Sigma_g)$. It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.

Setting

Let $G$ be a finite group. A surface tuple of genus $g$ in $G$ is a family $x=((x_1,y_1),\dots,(x_g,y_g))\in(G\times G)^g$. Its commutator product is

$$\mathrm{commProd}(x)=[x_1,y_1]\,[x_2,y_2]\cdots[x_g,y_g],\qquad [x,y]=xyx^{-1}y^{-1},$$

multiplied left to right. For $z\in G$ let $N_g(z)=\#\{x\in(G\times G)^g:\mathrm{commProd}(x)=z\}$ (commCount G g z). The surface group $\Gamma_g$ (SurfaceGroup g) is the presented group

$$\Gamma_g=\langle a_1,b_1,\dots,a_g,b_g\mid [a_1,b_1]\cdots[a_g,b_g]\rangle,$$

the standard presentation of the fundamental group of the closed orientable surface $\Sigma_g$ of genus $g$, whose Euler characteristic is $\chi(\Sigma_g)=2-2g$.

A complete irreducible family (IrrepFamily G ι) is a finite family $(V_i)_{i\in\iota}$ of finite-dimensional complex representations of $G$ that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some $V_i$. Write $d_i=\dim_{\mathbb C}V_i$ and $\chi_i(g)=\operatorname{tr}V_i(g)$ for the character.

Formalization targets

Goal: Mednykh's formula

For every finite group $G$, every complete irreducible family and every $g\ge 0$,

$$\sum_{i\in\iota} d_i^{\,2-2g}\;=\;|G|^{\,1-2g}\;\#\operatorname{Hom}(\Gamma_g,G),$$

which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with $\chi(S)=2-2g$. Equivalently, $\#\operatorname{Hom}(\Gamma_g,G)=|G|\sum_i(|G|/d_i)^{2g-2}$. Exponents are integers: at $g=0$ the formula reads $\sum_i d_i^2=|G|$.

Milestones

The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write $(x\star y)(w)=\sum_{\sigma\in G}x(w\sigma^{-1})\,y(\sigma)$ for the convolution of functions on $G$.

• M0. A complete irreducible family exists, with finite index type.
• M1. $\#\operatorname{Hom}(\Gamma_g,G)=N_g(1)$.
• M2. $\sum_i d_i\,\chi_i(z)=|G|$ if $z=1$ and $0$ otherwise.
• M3. For irreducible $V$ of dimension $d$: \sum_{a\in G}\chi_V(axa^{-1}y)=rac{|G|}{d}\chi_V(x)\chi_V(y).
• M4 (Mulase–Yu eq. (4.2)). For irreducible $V,W$: $\chi_V\star\chi_W$ equals rac{|G|}{d_V}\chi_V if $V\cong W$ and $0$ otherwise.
• M5 (Frobenius). $N_1(z)=|G|\sum_i\chi_i(z)/d_i$.
• M6. $N_{g_1+g_2}=N_{g_1}\star N_{g_2}$.
• M7 (Mulase–Yu Thm. 4.1). $N_g(z)=|G|^{2g-1}\sum_i\chi_i(z)\,d_i^{\,1-2g}$ for all $g\ge0$, $z\in G$. Mulase–Yu state it for $g\ge1$; the case $g=0$ is M2.

Significance

The result. The formula says that the number of $G$-coloured genus-$g$ surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example $D_4$ and $Q_8$, both with degrees $1,1,1,1,2$) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation $\varepsilon(h^{g})$ of the Frobenius algebra $Z(\mathbb C[G])$, where $h$ is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat $G$-bundles on $\Sigma_g$, and it underlies counts of covering spaces of surfaces.

Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.

Difficulty

The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, $\sum_i d_i\chi_i(z)=|G|\delta_{z,1}$. That relation is equivalent to the decomposition of the regular representation $\mathbb C[G]\cong\bigoplus_i V_i^{\oplus d_i}$, and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from $\operatorname{Hom}(\Gamma_g,G)$ to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general $G$.

Formalization scope

All representations are over $\mathbb C$: FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and $d_i$ is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on $g$ are integer powers (zpow) in $\mathbb C$, so $g=0$ is included and no natural-number truncation occurs. $\Gamma_g$ is PresentedGroup on generators Fin g × Bool, with $a_j=(j,\mathrm{false})$, $b_j=(j,\mathrm{true})$ and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for $\pi_1(\Sigma_g)$, since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.

Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.

Selected references

• N. Snyder, Mednykh's formula via lattice topological quantum field theories, arXiv:math/0703073 (2007). https://arxiv.org/abs/math/0703073
• A. D. Mednykh, Determination of the number of nonequivalent coverings over a compact Riemann surface, Dokl. Akad. Nauk SSSR 239 (1978) 269–271; English transl. Soviet Math. Dokl. 19 (1978) 318–320.
• R. Dijkgraaf, E. Witten, Topological gauge theories and group cohomology, Commun. Math. Phys. 129 (1990) 393–429. https://doi.org/10.1007/BF02096988
• D. S. Freed, F. Quinn, Chern–Simons theory with finite gauge group, Commun. Math. Phys. 156 (1993) 435–472. https://arxiv.org/abs/hep-th/9111004
• M. Mulase, J. T. Yu, A generating function of the number of homomorphisms from a surface group into a finite group, arXiv:math/0209008 (2002), §4 (algebraic proof). https://arxiv.org/abs/math/0209008
• M. Mulase, J. T. Yu, Non-commutative matrix integrals and representation varieties of surface groups in a finite group, Ann. Inst. Fourier 55 (2005) 1001–1036. https://arxiv.org/abs/math/0211127
• J. Kock, Frobenius Algebras and 2D Topological Quantum Field Theories, LMS Student Texts 59, Cambridge Univ. Press (2003). https://doi.org/10.1017/CBO9780511615443

Motivation

Compatibility of independently chosen row and column permutations controls how two families of local symmetries overlap. The source connects a weighted compatibility estimate to Thorp spectral bounds. The source is OpenAI's September 2026 manuscript.

Setting

A row system chooses a permutation in each row of an $A$ by $D$ array; a column system chooses a permutation in each column. They are compatible when their combined routing remains injective down each column. Nonnegative weights may bias each local permutation.

Formalization targets

$$\operatorname{WeightedCompatibility}(w,v)\le e^{C_0n^{54/100}}\prod_i M_\theta(w_i)\prod_j M_\theta(v_j),\qquad\theta=1-L/\log\sqrt n.$$

The proposition WeightedCompatibilityTheorem holds. Here, for natural numbers A and D, Rows assigns to each i in Fin A a permutation of Fin D, and Cols assigns to each j in Fin D a permutation of Fin A; a pair (r,c) is Compatible if for every column j the map i ↦ c(r_i(j))(i) is injective. The weightedCompatibility of real weight families w (indexed by i and a permutation of Fin D) and v (indexed by k and a permutation of Fin A) is (AD)! / ((D!)^A (A!)^D) times the uniform mean, over all pairs (r,c), of the indicator of compatibility times ∏_i w_i(r_i) ∏_k v_k(c_k). The marginalFactor for θ and a weight function u is the θ-th power of the uniform mean of u^(1/θ). The stated claim is that there exist reals L, C₀, m₀ > 0 such that for all natural numbers A and D, with n = AD, m = √n and θ = 1 − L/log m, whenever m ≥ m₀, θ > 0, and both A and D lie between m/2 and 2m, then for all nonnegative weight families w and v, weightedCompatibility(A,D,w,v) ≤ exp(C₀ n^(54/100)) · ∏_i marginalFactor(θ, w_i) · ∏_k marginalFactor(θ, v_k).

The goal is OAI.ThorpCompatibility.weightedCompatibility_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• remaining main.

Significance

The formal goal is an entropy-type inequality for arbitrary nonnegative local weights in sufficiently large balanced rectangles. It supplies a concrete combinatorial estimate that can support spectral analysis. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The compatibility indicator couples all row and column choices. A product of separate marginal expectations loses the injectivity constraint and cannot directly recover the stated exponent.

Formalization scope

The rectangle satisfies $n=AD$, with both side lengths between $\sqrt n/2$ and $2\sqrt n$. The theorem existentially chooses positive $L,C_0,m_0$ and assumes positive $\theta$. The marginal factor is the $\theta$th power of the uniform mean of the weight to power $1/\theta$.

The shared definitions are supplied by ThorpRemaining, ThorpWeightedCompatibility. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Compatibility entropy and the spectrum of a Thorp sweep, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The full permutation of a deck can remain far from uniform after each individual card is nearly uniform. The source analyzes Thorp mixing through representation estimates; the available goal isolates a reciprocal-dimension estimate and its Fourier consequence. The source is OpenAI's September 2026 manuscript.

Setting

A Specht module is a complex representation of a symmetric group associated with a partition. Sum the reciprocals of these dimensions over all partitions of $n$, and let $C_1$ be the supremum of these sums for positive $n$. A permutation distribution is compared with uniform through its averaged action on an irreducible representation.

Formalization targets

$$\sup_{n\ge1}\sum_{\lambda\vdash n}\frac1{\dim S^\lambda}<\infty,\qquad\|\widehat\nu(\rho)\|\le\sqrt{32C_1}(\dim\rho)^{-5/16}.$$

A conjunction of two parts. First, for each n let reciprocalFirst(n) be the sum, over all partitions p of n, of 1/deg(p), where deg(p) is the complex dimension of the Specht module of shape p (the span of the permutation-group translates of the polytabloid built from the canonical tableau, inside the space of tabloids). Let C1 be the supremum of reciprocalFirst(n) over n ≥ 1. The theorem asserts that this set of values is bounded above, that reciprocalFirst(n) ≤ C1 for every n ≥ 1, and that exceptionalFirst(n) tends to 0 as n → ∞, where exceptionalFirst(n) is the same sum of 1/deg(p) restricted to partitions p whose defect n − max(first row length, first column length) is positive. Second, for every d ≥ 3, every bijection e between the set of positions {0,1}^d (functions Fin d → Bool) and Fin 8 × Fin(2^(d−3)), every finite-dimensional complex inner product space E, and every irreducible complex representation ρ of the symmetric group on the positions, acting on E by inner-product-preserving maps, the following holds. Let ν be a probability distribution on this symmetric group (nonnegative values summing to 1) such that, for each i in Fin 8 and each group element g, the total ν-mass of the coset g·B_i is at most 4·|Sym(2^(d−3))|/|Sym(positions)|, where B_i is the subgroup of permutations that act through e by an arbitrary permutation of the i-th block of 2^(d−3) points and fix all other points. Then the operator norm of Σ_g ν(g)ρ(g) is at most √(32·C1)·(dim E)^(−5/16).

The goal is OAI.Thorp.Current.first_reciprocal_main.

Significance

The goal also proves that the reciprocal sum over shapes of positive defect tends to zero. The Fourier bound applies to distributions satisfying the specified eight-block coset-mass condition. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

One-card mixing does not control high-dimensional permutation representations. The bound must account for small-dimensional exceptional shapes and quantify contraction in every admissible irreducible representation.

Formalization scope

The Fourier clause has $d\ge3$, positions on a $d$-bit cube, a bijection into eight equal blocks, and unitary irreducible complex representations. Its coset-mass hypothesis is retained exactly. The target is a supporting representation estimate, not the paper’s final $1600d$-shuffle total-variation theorem.

The shared definitions are supplied by ThorpFirstReciprocal. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Optimal-order mixing of the Thorp shuffle, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation: when do partial observations of a permutation force full randomness?

Many random permutations are analysed through what they do to a few labels at a time: the joint positions of $k$ chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most $n-2$ labels, yet it is at total-variation distance $1/2$ from uniform on $S_n$. Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.

Timeline

• 1954 — Frame, Robinson and Thrall prove the hook-length formula for the degrees of irreducible representations of $S_n$ (Canad. J. Math. 1954).
• 1981 — Diaconis and Shahshahani analyse random transpositions by Fourier analysis on $S_n$, establishing the upper-bound-lemma framework (Z. Wahrsch. 1981).
• 2004 — Liebeck and Shalev show that the Witten zeta sums $\sum_{\lambda\vdash n}(f^\lambda)^{-u}$ tend to $2$ for every fixed $u>0$ (J. Algebra 2004).
• 2009, 2013 — Morris uses entropy and trajectory comparison to prove $O((\log n)^4)$ and $O((\log n)^3)$ mixing bounds for the Thorp shuffle (Ann. Probab. 2009; CPC 2013).
• 2014–2015 — Czumaj and Vöcking show that a fixed fraction of the cards randomizes in $O((\log n)^2)$ layers; Czumaj obtains full-permutation sampling by recursively applying partial randomizers on shrinking sets.
• 2026 — The OpenAI preprint From partial permutation information to Fourier bounds (OpenAI Math Release, September 26, 2026) proves that coset caps for complementary blocks control every Fourier matrix (Theorem 1.1). It has not been peer reviewed.

Setting

Let $X$ be a finite set of $n$ labels and $G=\mathrm{Sym}(X)$, acting as maps from initial labels to final positions. For $M\subseteq X$, let $H_M\le G$ be the block subgroup of permutations that fix every label outside $M$. Two permutations have the same images on $X\setminus M$ exactly when they lie in the same left coset $gH_M$, so a bound on the law of those images is a bound on coset masses.

For a nonnegative weight $f$ on $G$ and a unitary representation $\rho$ of $G$ on a finite-dimensional complex inner-product space $V$, the Fourier transform is $\widehat f(\rho)=\sum_{g\in G}f(g)\rho(g)$, with $D=\dim V$. The Hilbert–Schmidt norm is unnormalized, $\|A\|_{\mathrm{HS}}^2=\operatorname{tr}(A^*A)$. For $u>0$ the symmetric degree constant is

$$C_u=\sup_{m\ge1}\ \sum_{\lambda\vdash m} D_\lambda^{-u},$$

where $D_\lambda$ ranges over the degrees of the irreducible complex representations of $S_m$.

Formalization targets

Goal: complementary cosets control Fourier matrices (Theorem 1.1)

Partition $X$ into $b\ge1$ nonempty blocks $M_1,\dots,M_b$ and put $H_i=H_{M_i}$. Let $f\ge0$ on $G$ have total mass at most one and satisfy

$$f(gH_i)\le \frac{B}{[G:H_i]}\qquad(g\in G,\ 1\le i\le b).$$

Then for every $u>0$ and every irreducible unitary $\rho$ of degree $D$,

$$\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b} \qquad\text{and}\qquad \|\widehat f(\rho)\|_{\mathrm{op}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b}.$$

No restriction is placed on the block sizes or on multiplicities in the restriction of $\rho$ to $H_1\times\dots\times H_b$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of $S_n$. With $b=8$ and $u=1$ it gives $\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le 8C_1D^{-5/8}$, which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of $7n/8$ labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in $O(\log n)$ shuffles. The statement concerns arbitrary laws on $S_n$ and does not depend on any shuffle.

Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.

Difficulty

The natural approach decomposes $\rho$ restricted to $H_1\times\dots\times H_b$ into tensor products of irreducibles of the blocks and bounds $\widehat f(\rho)$ on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in $D$. The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant $C_u$ is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.

Formalization scope

• $X$ is an arbitrary Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.
• The coset cap is LeftCosetCap f H B: for every $g$, $\sum_{h\in H}f(gh)\le B/[G:H]$, with the index H.index.
• $\rho$ is any irreducible representation on a finite-dimensional complex inner-product space with $\langle\rho(g)x,\rho(g)y\rangle=\langle x,y\rangle$; the Fourier transform is complexFourier ρ f; hsNormSq is $\operatorname{Re}\operatorname{tr}(A^*A)$; the operator norm is that of the associated continuous linear map; $D$ is Module.finrank ℂ V and the exponent is a real power.
• Irreducible representations of $S_m$ are indexed by the isotypic components of the regular representation of Equiv.Perm (Fin m), and $C_u$ is symmetricDegreeConstant u, an sSup over $m\ge1$. The supremum is finite for every $u>0$; a solver must prove this boundedness, since sSup of an unbounded real set would be $0$.
• Needed infrastructure: isotypic decomposition and Schur's lemma for finite groups, degree bounds for $S_m$ (hook-length or tableau counting), and uniform Witten zeta bounds. The degree layer is reusable for any random walk on $S_n$.

Selected references

• J. S. Frame, G. de B. Robinson and R. M. Thrall, The hook graphs of the symmetric group, Canad. J. Math. 6 (1954), 316–324. https://doi.org/10.4153/CJM-1954-030-1
• P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981), 159–179. https://doi.org/10.1007/BF00535487
• G. D. James, The Representation Theory of the Symmetric Groups, Lecture Notes in Math. 682, Springer, 1978.
• B. E. Sagan, The Symmetric Group, 2nd ed., Graduate Texts in Math. 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
• M. W. Liebeck and A. Shalev, Fuchsian groups, coverings of Riemann surfaces, subgroup growth, random quotients and random walks, J. Algebra 276 (2004), 552–601. https://doi.org/10.1016/S0021-8693(03)00515-5
• E. O. Thorp, Nonrandom shuffling with applications to the game of faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• A. Czumaj and B. Vöcking, Thorp shuffling, butterflies, and non-Markovian couplings, ICALP 2014, LNCS 8572, 344–355. https://doi.org/10.1007/978-3-662-43948-7_29
• A. Czumaj, Random permutations using switching networks, STOC 2015, 703–712. https://doi.org/10.1145/2746539.2746629
• OpenAI, From partial permutation information to Fourier bounds, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 1–2; Corollary 3.6, p. 9). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/From-partial-permutation-information-to-Fourier-bounds-September-26-2026/main.pdf

Motivation: plethysm, Foulkes' conjecture and the canonical map

Plethysm — decomposing $\operatorname{Sym}^a(\operatorname{Sym}^b V)$ into irreducible $\mathrm{GL}(V)$-representations — is one of the oldest open problems in the representation theory of the general linear group, and it is central to geometric complexity theory, where the coordinate rings of Chow varieties of products of linear forms control lower-bound arguments. Foulkes' conjecture (1950) predicts that for $a\le b$ there is a $\mathrm{GL}(V)$-equivariant injection $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$. A natural candidate is supplied by a specific map, the canonical Foulkes–Howe map $\mu_{a,b,V}:\operatorname{Sym}^b(\operatorname{Sym}^aV)\to\operatorname{Sym}^a(\operatorname{Sym}^bV)$; its surjectivity yields such an embedding by complete reducibility. Its image is the degree-$b$ part of the coordinate ring of the Chow variety of decomposable $a$-forms, so surjectivity for large $b$ is a statement about that variety's normalization. The question is from which degree $b$ on the map is surjective, uniformly in $\dim V$.

Timeline

• 1950 — Foulkes formulates the plethysm comparison (Foulkes, J. London Math. Soc. 1950).
• 1993 — Brion proves eventual surjectivity of the canonical map for fixed $a$ and $V$ (Brion, Manuscripta Math. 1993); in 1997 he gives an effective bound depending on both $a$ and $\dim V$ (Séminaires et Congrès 2, SMF, 1997, Theorem 3.3).
• 2008 — McKay proves a propagation theorem for Foulkes-type injectivity (J. Algebra 2008); Ikenmeyer gives a weight-shift proof (arXiv:1509.04957, 2015).
• 2015 — Landsberg's introduction to geometric complexity theory asks for a polynomial stabilization bound (Problem 7.19) (Ann. Univ. Ferrara 2015).
• 2017 — Cheung, Ikenmeyer and Mkrtchyan show that the canonical map has nonzero kernel at $(a,b)=(5,5)$ and $(6,6)$ in suitable dimensions (J. Symbolic Comput. 2017).
• 2022 — Raicu, Sam and Weyman bound the regularity of the Segre ring and modules of covariants on the Chow variety (Vietnam J. Math. 2022), without computing the top degree controlling stabilization.
• 2026 — An OpenAI preprint, Quadratic stabilization of the canonical Foulkes–Howe map (OpenAI Math Release, September 25, 2026), claims surjectivity for all $a\ge2$, $b\ge a(a-1)$ and every finite-dimensional $V$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Let $V$ be a finite-dimensional complex vector space and $\operatorname{Sym}V$ its symmetric algebra. $\operatorname{Sym}^nV\subseteq\operatorname{Sym}V$ is the span of products $v_1\cdots v_n$ of $n$ vectors. For $v_{j,i}\in V$ ($1\le j\le b$, $1\le i\le a$), the canonical Foulkes–Howe map is the linear map determined by

$$\mu_{a,b,V}\Bigl(\prod_{j=1}^{b}\bigl(v_{j,1}\cdots v_{j,a}\bigr)\Bigr) =\frac{1}{(a!)^{b}}\sum_{\sigma_1,\dots,\sigma_b\in S_a}\ \prod_{i=1}^{a}\Bigl(\prod_{j=1}^{b}v_{j,\sigma_j(i)}\Bigr),$$

where the outer products on the left and right are taken in $\operatorname{Sym}(\operatorname{Sym}^aV)$ and $\operatorname{Sym}(\operatorname{Sym}^bV)$ respectively. Equivalently: identify $\operatorname{Sym}^aW$ with symmetric tensors via averaging, multiply $b$ such tensors in $(\operatorname{Sym}V)^{\otimes a}$, and project back. That this formula is well defined on $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is part of the content.

Formalization targets

Goal: quadratic stabilization (Theorem 1)

For every finite-dimensional complex $V$ and integers $a\ge2$, $b\ge a(a-1)$, there is a unique linear map

$$\mu:\operatorname{Sym}^b(\operatorname{Sym}^aV)\longrightarrow\operatorname{Sym}^a(\operatorname{Sym}^bV)$$

satisfying the displayed formula on monomials, and $\mu$ is surjective.

The bound $a(a-1)$ is not claimed to be sharp; the content is a stabilization degree polynomial in $a$ and independent of $\dim V$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Surjectivity gives, by complete reducibility, a $\mathrm{GL}(V)$-equivariant embedding $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$ for $b\ge a(a-1)$ (Corollary 4 of the source), e.g. the sixth-power comparison for $b\ge30$. It answers positively the request for a polynomial bound in Landsberg's Problem 7.19, and it says that the coordinate ring of the Chow variety of decomposable $a$-forms agrees with its normalization in every degree $b\ge a(a-1)$. Since the canonical map is known to fail to be injective at $(5,5)$ and $(6,6)$, an explicit range of surjectivity is the right kind of statement for this specific map.

Formalizing it. The statement is purely algebraic and uniform in $V$, $a$, $b$. A formal proof would need multilinear algebra over symmetric algebras (symmetric powers of symmetric powers), which is reusable for plethysm and invariant-theory projects.

Difficulty

Surjectivity is equivalent to the vanishing of every symmetric $a$-linear form on $\operatorname{Sym}^bV$ whose diagonal vanishes on products of $b$ vectors. The naive induction on $a$ fails because the factors in different slots share a common product and cannot be varied independently; the dimension of $V$ also grows the space of such forms without bound, so arguments using a fixed basis or dimension count do not give a uniform bound. Brion's effective bound depends on $\dim V$, and regularity bounds for the normalization do not locate the top degree of the quotient that controls stabilization.

Formalization scope

• $\operatorname{Sym}^nV$ is represented as the submodule SymPow n V of Mathlib's SymmetricAlgebra ℂ V spanned by products of $n$ vectors, and $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is SymPow b (SymPow a V).
• IsFoulkesMap a b V μ states the monomial formula above, with the normalizing factor $(a!)^{-b}$ and the sum over $b$-tuples of permutations of Fin a.
• The goal asserts existence, surjectivity and uniqueness of a linear map with this formula; uniqueness rules out choosing an arbitrary surjection, so the theorem is about the canonical map and not merely about dimensions.
• $V$ ranges over all finite-dimensional complex vector spaces in an arbitrary universe; $a\ge2$ and $b\ge a(a-1)$ are natural numbers.
• Needed infrastructure: symmetric powers inside the symmetric algebra, polarization/annihilator criteria, and directional-derivative operators on polynomial functions.

Selected references

• H. O. Foulkes, Concomitants of the quintic and sextic up to degree four in the coefficients of the ground form, J. London Math. Soc. 25 (1950), 205–209. https://doi.org/10.1112/jlms/s1-25.3.205
• M. Brion, Stable properties of plethysm: on two conjectures of Foulkes, Manuscripta Math. 80 (1993), 347–371. https://doi.org/10.1007/BF03026558
• M. Brion, Sur certains modules gradués associés aux produits symétriques, Séminaires et Congrès 2, SMF, 1997, 157–183. https://smf.emath.fr/publications/sur-certains-modules-gradues-associes-aux-produits-symetriques
• T. McKay, On plethysm conjectures of Stanley and Foulkes, J. Algebra 319 (2008), 2050–2071. https://doi.org/10.1016/j.jalgebra.2007.12.003
• C. Ikenmeyer, On McKay's propagation theorem for the Foulkes conjecture, arXiv:1509.04957, 2015. https://arxiv.org/abs/1509.04957v1
• J. M. Landsberg, Geometric complexity theory: an introduction for geometers, Ann. Univ. Ferrara 61 (2015), 65–117. https://doi.org/10.1007/s11565-014-0202-7
• M.-W. Cheung, C. Ikenmeyer and S. Mkrtchyan, Symmetrizing tableaux and the 5th case of the Foulkes conjecture, J. Symbolic Comput. 80 (2017), 833–843. https://doi.org/10.1016/j.jsc.2016.09.002
• C. Raicu, S. V. Sam and J. Weyman, On some modules supported in the Chow variety, Vietnam J. Math. 50 (2022), 501–521. https://doi.org/10.1007/s10013-021-00527-2
• OpenAI, Quadratic stabilization of the canonical Foulkes–Howe map, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf

Motivation

The permanent versus determinant problem asks how large an $n$ must be for the permanent of an $m \times m$ matrix to be written as the determinant of an $n \times n$ matrix whose entries are affine linear functions of the $m^2$ input variables. Valiant showed that some finite $n$ always works and conjectured in 1979 that the least such $n$, the determinantal complexity $\mathrm{dc}(\mathrm{per}_m)$, grows faster than every polynomial in $m$; this is the algebraic counterpart of $\mathbf{P} \ne \mathbf{NP}$.

Geometric complexity theory (GCT), proposed by Mulmuley and Sohoni in 2001, attacks the conjecture by replacing the two polynomials with the closures of their $\mathrm{GL}$-orbits and comparing the $\mathrm{GL}$-representations carried by the coordinate rings of those closures. If some irreducible representation occurs in the coordinate ring of the orbit closure of the padded permanent but not in that of the determinant, then one orbit closure cannot contain the other, and a lower bound on $\mathrm{dc}(\mathrm{per}_m)$ follows. Such a representation is an occurrence obstruction, and Mulmuley and Sohoni conjectured that occurrence obstructions exist for every polynomial padding.

Timeline of what is actually proved.

• 1979: Valiant introduces $\mathrm{dc}$ and conjectures superpolynomial growth (Valiant 1979).
• 2001: Mulmuley and Sohoni restate the conjecture in terms of orbit closures and propose proving it by exhibiting occurrence obstructions (arXiv:cs/9908014).
• 2014: Kadish and Landsberg show that any partition occurring for the padded permanent has at most $m^2$ rows and a first row of length at least $(n-m)d$ (arXiv:1204.4772).
• 2016: Ikenmeyer and Panova show that vanishing rectangular Kronecker coefficients cannot supply occurrence obstructions (arXiv:1512.03798).
• 2016: Mulmuley, in GCT V, makes the "infinitesimally close approximation" form of the permanent hardness hypothesis the engine of derandomized Noether normalization (JAMS).
• 2017: Ikenmeyer, Mulmuley and Walter prove that deciding positivity of Kronecker coefficients is $\mathbf{NP}$-hard and construct superpolynomially many vanishing triples in the Kronecker cone (comput. complex. 26).
• 2019: Bürgisser, Ikenmeyer and Panova prove that no occurrence obstructions exist at all once $n \ge m^{25}$, refuting the Mulmuley–Sohoni conjecture on obstructions (JAMS 32).

Setting

Fix $n$ and write $V = \mathbb{C}^{n \times n}$. A form of degree $n$ is a homogeneous polynomial of degree $n$ in the $n^2$ variables $X_{ij}$, $0 \le i, j < n$; the space of such forms is $\mathrm{Sym}^n V^*$. The group $\mathrm{GL}_{n^2}$ acts on it by linear substitution of the variables, and for a form $p$ we write $\overline{\mathrm{GL}_{n^2}\cdot p}$ for the closure of its orbit in the Euclidean topology, which for these orbits agrees with the Zariski closure.

Two orbit closures matter:

$$\Omega_n \;=\; \overline{\mathrm{GL}_{n^2}\cdot \det\nolimits_n}, \qquad Z_{n,m} \;=\; \overline{\mathrm{GL}_{n^2}\cdot X_{00}^{\,n-m}\mathrm{per}_m},$$

where $\det_n = \sum_{\sigma \in S_n}\mathrm{sgn}(\sigma)\prod_i X_{i\sigma(i)}$ and $\mathrm{per}_m = \sum_{\sigma \in S_m}\prod_i X_{i\sigma(i)}$, and the second polynomial is padded by a power of the single variable $X_{00}$ so that it, too, has degree $n$.

The coordinate ring of a $\mathrm{GL}_{n^2}$-stable subset $S$ of $\mathrm{Sym}^n V^*$ decomposes into irreducible polynomial representations, which are labelled by partitions $\lambda$ with at most $n^2$ parts. A partition $\lambda \vdash nd$ occurs in the degree $d$ part of the coordinate ring of $S$ when some polynomial function $F$ of degree $d$ on $\mathrm{Sym}^n V^*$ is an eigenvector of the Borel subgroup of upper triangular matrices,

$$F(g \cdot p) \;=\; \Big(\prod_{v} g_{vv}^{\lambda_{v}}\Big) F(p) \quad\text{for all upper triangular invertible } g \text{ and all forms } p,$$

and $F$ does not vanish identically on $S$. If $\lambda$ occurs for $Z_{n,m}$ but not for $\Omega_n$, then $Z_{n,m} \not\subseteq \Omega_n$, hence $\mathrm{dc}(\mathrm{per}_m) > n$: this is an occurrence obstruction.

Formalization targets

Goal — no occurrence obstructions (Theorem 1.4)

$$n \ge m^{25},\quad \lambda \vdash nd, \quad \lambda \text{ occurs for } Z_{n,m} \;\Longrightarrow\; \lambda \text{ occurs for } \Omega_n .$$

No partition can separate the two orbit closures once the padding is at least polynomial of degree $25$; the occurrence-obstruction route to Valiant's conjecture is therefore closed.

Supporting targets

The milestone list follows the structure of the proof: the shape restriction for the padded permanent (Theorem 2.1), the semigroup property of occurring partitions (Lemma 2.2), the occurrence of row extended even rectangles (Proposition 2.3), the non-vanishing of highest weight vectors of long first row on $\Omega_n$ (Proposition 2.4), and the fact that padded power sums lie in $\Omega_n$ (Theorem 2.5), together with two elementary anchors ($\Omega_2$ is everything; a symbolic determinant of size $n$ puts the padded permanent into $\Omega_n$) and the GCT V hardness hypothesis, which is exactly the statement that the padded permanent stays outside $\Omega_s$ for subexponential $s$.

Significance

Theorem 1.4 removes an entire proof strategy: after fifteen years in which occurrence obstructions were the main object of study in GCT, the theorem shows that they do not exist in the regime where they would be useful, so lower bounds must come from comparing multiplicities rather than mere occurrence. The supporting statements are of independent use: Theorem 2.5 and Proposition 2.3 give explicit families of points and partitions for $\Omega_n$, and the shape restriction of Theorem 2.1 constrains every future obstruction argument.

None of this is formalized anywhere. What this mission produces is a machine-checked model of orbit closures of forms, of the Borel-eigenvector description of occurrence, and of the known statements about $\Omega_n$ and $Z_{n,m}$ — infrastructure that any later multiplicity-based argument would reuse. The goal theorem is proved in the literature; the work here is formalizing that proof. The hardness hypothesis and the Mulmuley–Sohoni conjecture itself remain open, and are labelled as such.

Difficulty

The naive approach to "λ occurs in $\mathbb{C}[\Omega_n]$" is to decompose the plethysm $\mathrm{Sym}^d \mathrm{Sym}^n V$ and read off multiplicities; this fails because the coordinate ring of $\Omega_n$ is a quotient of that plethysm by the unknown vanishing ideal of the orbit closure, and almost nothing is known about which highest weight vectors survive restriction. The proof of Theorem 1.4 works instead with explicit highest weight vectors evaluated at explicit points of $\Omega_n$ (padded power sums), using the fundamental invariant of $\mathrm{Sym}^n \mathbb{C}^N$ and a lifting map for highest weight vectors in plethysms; the combinatorics of tableaux and the case distinction on the degree $d$ are where the work lies. A formalization additionally has to build the representation-theoretic vocabulary from scratch, since Mathlib has neither plethysms, nor Weyl modules, nor highest weight theory for $\mathrm{GL}_N$.

Formalization scope

Conventions fixed by the Lean development, all in the namespace GCTOcc:

1. Polynomials live in one ring, with variables indexed by pairs of natural numbers; the $n \times n$ matrix of variables occupies the indices $i, j < n$, so forms of different sizes need no renaming maps.
2. The padding variable is $X_{00}$, an entry of the matrix itself, as in the source; the choice of padding linear form is known to be immaterial.
3. Orbit closure is defined sequentially: $p$ lies in the closure when the coefficients of a sequence of orbit points converge to those of $p$. On this finite-dimensional space sequential closure is the Euclidean closure.
4. Occurrence of $\lambda$ is defined by the existence of a Borel eigenvector of weight $\lambda$ and degree $d$ that does not vanish identically on the set. Weights are indexed by the order $(i,j) \mapsto in+j$ on the variables, and triangularity refers to the same order. A partition is a nonincreasing function $\mathbb{N} \to \mathbb{N}$ supported on the first $n^2$ indices whose parts sum to $nd$.
5. The statements are not vacuous: all hypotheses used in the milestones are satisfiable, and the elementary anchors ($\Omega_2$, the symbolic determinant bridge) exhibit points of the orbit closures explicitly.

Infrastructure a complete development needs, and which is reusable beyond this mission: plethysms $\mathrm{Sym}^d\mathrm{Sym}^n V$ and their highest weight vectors, the fundamental invariant of a form space, semistandard tableaux of rectangular content, and basic facts about orbit closures of forms. Contributions of any of these pieces are welcome, as are counterexample-hunting reports on the elementary anchors.

Not covered here: the Kronecker-coefficient strand of the program (Ikenmeyer–Mulmuley–Walter 2017 on $\mathbf{NP}$-hardness of Kronecker positivity, and the construction of vanishing triples in the Kronecker cone). Stating those results requires irreducible characters of the symmetric group indexed by partitions, or equivalently symmetric-function machinery, which Mathlib does not yet have; they are natural targets for a companion mission once Specht modules exist.

Selected references

• P. Bürgisser, C. Ikenmeyer, G. Panova, No occurrence obstructions in geometric complexity theory, J. Amer. Math. Soc. 32 (2019), 163–193, doi:10.1090/jams/908.
• K. D. Mulmuley, Geometric Complexity Theory V: Efficient algorithms for Noether normalization, J. Amer. Math. Soc., electronically published 2016, doi:10.1090/jams/864.
• C. Ikenmeyer, K. D. Mulmuley, M. Walter, On vanishing of Kronecker coefficients, comput. complex. 26 (2017), doi:10.1007/s00037-017-0158-y.
• L. G. Valiant, Completeness classes in algebra, STOC 1979, doi:10.1145/800135.804419.
• H. Kadish, J. M. Landsberg, Padded polynomials, their cousins, and geometric complexity theory, Comm. Algebra 42 (2014), arXiv:1204.4772.