Representation Theory

Motivation

Finitely many rotations of the sphere generate a group whose orbits are typically dense. A basic quantitative question is how fast those orbits fill the sphere: after words of length $\ell$ in the generators, how uniformly are the points spread? The answer is controlled by the spectral gap of an averaging operator built from the generators. The question goes back to the Banach–Ruziewicz problem (uniqueness of rotation-invariant finitely additive measures on spheres), was studied by Lubotzky, Phillips and Sarnak in their work on distributing points on $S^2$ (LPS 1987), and was formulated as a conjecture about random generators by Gamburd, Jakobson and Sarnak. It also matters in quantum computing: a spectral gap for a gate set gives efficient approximation of every single-qubit gate by short gate sequences (Sawicki–Karnas 2017).

Timeline.

• 1987 — Lubotzky, Phillips and Sarnak construct explicit rotations with optimal spectral gap using automorphic forms and pose the general question (LPS).
• 2006 — Fisher proves a zero–one law: for $n \ge 3$ generators, either almost every $n$-tuple has a spectral gap or almost every $n$-tuple has none (Fisher, IMRN 2006, arXiv:math/0601050).
• 2008 — Bourgain and Gamburd prove the spectral gap for elements of $SU(2)$ with algebraic entries generating a free group (Invent. Math. 171).
• 2012 — Bourgain and Gamburd extend this to dense subgroups of $SU(d)$, $d \ge 2$, generated by finitely many elements with algebraic entries (JEMS 14, arXiv:1108.6264).

The tuples with algebraic entries form a Haar-null set, so the conjecture for random tuples remains open.

Setting

Let $SU(d)$ be the group of complex $d\times d$ matrices $U$ with $U^*U = UU^* = I$ and $\det U = 1$, a compact group with its normalized Haar measure $\mu_d$ (the unique left-invariant Borel probability measure). For $g_1,\dots,g_n \in SU(d)$ the Hecke operator acts on functions $f : SU(d) \to \mathbb C$ by

$$(z_g f)(x) = \sum_{j=1}^{n} \bigl( f(g_j x) + f(g_j^{-1} x) \bigr).$$

On $L^2(SU(d),\mu_d)$ it is bounded and self-adjoint, constants are eigenfunctions with eigenvalue $2n$, and it preserves the space $L^2_0$ of mean-zero functions. Writing $\lambda_1(z_g)$ for the supremum of the spectrum of $z_g$ on $L^2_0$, one always has $\lambda_1 \le 2n$, and $z_g$ (or the tuple $g$) has a spectral gap when

$$\lambda_1(z_g) < 2n .$$

For $SU(2)$, each $U$ acts on the sphere $S^2$ by rotations, and $z_g$ is the operator $\phi_{U_1} + \phi_{U_1}^{-1} + \dots + \phi_{U_n} + \phi_{U_n}^{-1}$ of the source.

Formalization targets

Goal: the spectral gap conjecture

For every $n > 2$, if $U_1,\dots,U_n$ are chosen independently and uniformly (Haar) at random in $SU(2)$, then with probability $1$

$$\lambda_1\bigl(z_{U_1,\dots,U_n}\bigr) < 2n .$$

Milestones from the literature

1. Fisher's zero–one law (2006, Theorem 1.2): for $n \ge 3$, either almost every $n$-tuple has a spectral gap, or almost every $n$-tuple has none.
2. Bourgain–Gamburd in $SU(2)$ (2008): tuples with algebraic entries (up to simultaneous conjugation) that freely generate a free group of rank $n\ge 2$ have a spectral gap.
3. Bourgain–Gamburd in $SU(d)$ (2012, Theorem 1): for $d \ge 2$, tuples with algebraic entries generating a dense subgroup of $SU(d)$ have a spectral gap.

By Fisher's law, the goal follows once a spectral gap is shown on a set of positive Haar measure.

Significance

A spectral gap for $g$ means that random walks driven by $g_1^{\pm1},\dots,g_n^{\pm1}$ equidistribute in $SU(2)$ (and orbits equidistribute on $S^2$) at an exponential rate, and that the action of the generated group on $S^2$ is strongly ergodic. In quantum computation it says that a universal single-qubit gate set is automatically efficiently universal. The conjecture asserts that this holds for a typical gate set, not just for the arithmetically special ones covered by Bourgain–Gamburd.

On the formal side, the milestones are proved theorems (Fisher; Bourgain–Gamburd) that have, to the knowledge of this proposal, no machine-checked proofs. Formalizing any of them requires substantial new libraries: Haar measure and harmonic analysis on $SU(d)$, ergodicity of $\mathrm{Aut}(F_n)$ on $\mathrm{Hom}(F_n, SU(2))$ (Goldman), and the arithmetic-combinatorial machinery of Bourgain–Gamburd. The goal itself is an open problem.

Difficulty

Spectral gap is not detected by density alone: every tuple generating a dense subgroup gives an ergodic action, but ergodicity only shows $\lambda_1$ is not an eigenvalue, not that it is bounded away from $2n$. Known proofs need either arithmetic structure (automorphic forms, or the algebraic entries used by Bourgain–Gamburd to rule out short relations that come too close to the identity) or rigidity (property (T)). A generic tuple has neither.

Formalization scope

• $SU(d)$ is Matrix.specialUnitaryGroup (Fin d) ℂ with the subspace topology and its Borel σ-algebra; it is shown to be a compact topological group, and haarSU d is the Haar measure normalized to total mass $1$.
• The Hecke operator acts on all functions $f : SU(d) \to \mathbb C$ by the formula above.
• "Spectral gap" is encoded through the quadratic form: there is $\varepsilon > 0$ such that $\operatorname{Re}\langle z_g f, f\rangle \le (2n-\varepsilon)\,\|f\|_2^2$ for every $f \in L^2$ with $\int f\,d\mu = 0$. For a bounded self-adjoint operator this is exactly $\lambda_1 < 2n$ (one-sided gap, as in Fisher and Bourgain–Gamburd).
• "Chosen uniformly at random" is the product Haar measure on $SU(2)^n$; "with probability $1$" is an almost-everywhere statement.
• The goal is stated on $L^2(SU(2))$, as in the source. The operator on $L^2(S^2)$ is the restriction to a subrepresentation, so a gap on $L^2_0(SU(2))$ implies a gap on $L^2_0(S^2)$. Fisher (2006, §1) remarks that the two versions of the conjecture are equivalent.
• Trivializations are ruled out: for $g_1=\dots=g_n=I$ the quadratic form equals $2n\|f\|^2$, so no gap holds, and for $n=0$ the gap fails as well.

Useful reusable contributions include: basic harmonic analysis on compact groups (translation invariance in $L^2$, self-adjointness of $z_g$), the Peter–Weyl decomposition of $L^2(SU(2))$, conjugation invariance of the gap, and monotonicity of the gap in the generating set.

Selected references

• A. Lubotzky, R. Phillips, P. Sarnak, Hecke operators and distributing points on $S^2$. II, Comm. Pure Appl. Math. 40 (1987). https://doi.org/10.1002/cpa.3160400402
• D. Fisher, $\mathrm{Out}(F_n)$ and the spectral gap conjecture, IMRN 2006. https://doi.org/10.1155/IMRN/2006/26028 (arXiv:math/0601050)
• J. Bourgain, A. Gamburd, On the spectral gap for finitely-generated subgroups of $SU(2)$, Invent. Math. 171 (2008). https://doi.org/10.1007/s00222-007-0072-z
• J. Bourgain, A. Gamburd, A spectral gap theorem in $SU(d)$, J. Eur. Math. Soc. 14 (2012). https://doi.org/10.4171/jems/337 (arXiv:1108.6264)
• A. Sawicki, K. Karnas, Criteria for universality of quantum gates, Phys. Rev. A 95 (2017). https://doi.org/10.1103/PhysRevA.95.062303
• Wikipedia, Spectral gap conjecture. https://en.wikipedia.org/wiki/Spectral_gap_conjecture

Motivation

Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.

Setting

The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.

Formalization target

The selected goal is OAI.MinimalVertex.main. Its central assertion is

$$\mathrm{energy\ bounds}\ \land\ \mathrm{strong\ locality}\ \land\ \mathrm{irreducible\ conformal\ net}.$$

The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.

Significance and status

The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Strongly rational unitary vertex operator algebras and conformal nets, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.

Setting

A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.

Formalization targets

$$\log\!\left(\dim S^\lambda\,\operatorname{Re}\operatorname{tr}(Q^*Q)^r\right)\le a(\eta,d)H(\alpha,\beta)+R(\kappa,d,\ell).$$

There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).

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

• one sided type angle.
• remaining main.

Significance

The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. 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

Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.

Formalization scope

The quantifier order is $\eta_0$, then each small $\eta$, then $\kappa_0<\eta/256$, then each small $\kappa$, then one positive integer $r$. Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.

The shared definitions are supplied by SignedSweepMoment, SpinAngle, ThorpRemaining. 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, Signed tensor densities and diagram budgets for the Thorp shuffle, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Row and column symmetries organize how permutation representations respond to a coordinate sweep. The source seeks dimension-dependent contraction strong enough to control the full deck. The source is OpenAI's September 2026 manuscript.

Setting

For a Young diagram $\mu$, let $D$ be its Specht dimension and $Q$ its averaged sweep operator. A Schatten norm measures all singular values, not only the largest one. The goal seeks one weight function on diagrams and a uniformly bounded family of norm exponents.

Formalization targets

$$D^{3/4}\le W(\mu)\le D,\quad W(\mu)\|Q\|_{p(d)}^{p(d)}\le1,\quad\|Q\|\le D^{-3/(4p_*)},\quad2\le p(d)\le p_*.$$

There exist a function W assigning a strictly positive real weight to every Young diagram, a real constant pStar ≥ 2, and exponents p(d) for each d ≥ 1 with 2 ≤ p(d) ≤ pStar, such that the following holds for every d ≥ 1 and every Young diagram μ with exactly 2^d cells. Let dim(μ) be the complex dimension of the Specht module of μ, spanned by the translates of the polytabloid in the permutation space on tabloids of μ, regarded as a Hilbert subspace. Let the Fourier sweep be the average, over all sequences ω of d coin configurations, of the unitary operator by which the product of d card-shuffling steps run(d,d)(ω) acts on this space; each step composes a cyclic rotation of the d-bit positions with a pair switch that flips the first bit according to a coin function of the remaining bits, and the 2^d card positions are identified with the cells of μ by a fixed bijection. Then dim(μ)^(3/4) ≤ W(μ) ≤ dim(μ); W(μ) times the p(d)-th power of the Schatten p(d)-norm of the Fourier sweep (the p(d)-th root of the sum of the p(d)-th powers of its singular values) is at most 1; and the operator norm of the Fourier sweep is at most dim(μ)^(-3/(4·pStar)). The proof is admitted in the source rather than established.

The goal is OAI.CubeShuffle.WeightedSweep.weighted_sweep_moments. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• occupied overlap.
• occupied overlap endpoint.

Significance

The target gives both a weighted singular-value estimate and an operator-norm consequence. These quantify contraction across representations of widely differing dimensions. 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

An operator norm bound alone does not control the dimension-weighted sum of all modes. The weight and Schatten exponent must be chosen uniformly across every diagram of size $2^d$.

Formalization scope

The goal is weighted_sweep_moments, with $d\ge1$, positive diagram weights, and one finite upper exponent $p_*$. The finite-dimensional complex inner-product representations and the physical $d$-step sweep are those of the supplied definitions.

The shared definitions are supplied by OccupiedOverlap, WeightedSweepMoments. 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, Row–column symmetry and contraction of coordinate sweeps, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The routing paths of different cards share switches. The source controls the resulting dependence through partial-permutation densities and representation contraction. The source is OpenAI's September 2026 manuscript.

Setting

Positions form a binary cube. A sweep operator averages the Specht-module action of all switch outcomes. The defect of a Young diagram is its number of cells outside the first row, and the level scale is $k(1+\log(n/k))$.

Formalization targets

$$\text{adaptive bounds}\ \wedge\ \text{Casimir bounds}\ \wedge\ \text{dense truncation}\ \wedge\ \text{sparse contact}\ \wedge\ \text{harmonic bounds}\ \wedge\ \text{smoothing}\ \wedge\ \text{tail bounds}\ \wedge\ \text{high-tail bounds}\ \wedge\ \text{sparse saving}.$$

The theorem states, as an admitted result, that nine separate formal statements about Thorp-shuffle routing hold simultaneously. Throughout, Card d is the set of d-bit strings (the 2^d cards), the sweep operator of a Young diagram mu (with the d bits relabelled to its cells by a bijection e) is the average over all butterfly switch settings of the Specht-module action of the butterfly permutation (or of its inverse, if the reverse flag is set), k = |mu| minus the first row length measures how far mu is from a single row, and the level scale of n and k is k(1+log(n/k)). (1) Adaptive: for some positive constants c, c', C, c0, for every d, mu, e and reverse flag, with h the level scale of 2^d and k, and D the dimension of the Specht module, the norm of the positive square F = S S* of the sweep operator S is at most exp(-c h), the trace of F^4 is at most exp(-c' log D + C h), and the norm of S is at most exp(-c0 (log D + h)). (2) Casimir: for some positive a and C, the palindrome row moment of order 1/64, raised to 64/65, is at most exp(C times level scale) for every injective k-tuple of cards; for every mu with k>0, the operator norm of the palindrome-shuffle operator K is at most exp(-a times level scale) and dim(Specht module) times the real trace of K^65 is at most exp(C times level scale); and for some positive integer l, from any starting permutations the total variation distance of the law of ld shuffle steps from uniform on all permutations of 2^d cards tends to 0 as d tends to infinity. (3) Dense truncation: for every density rho>0 and epsilon>0 there is c>0 such that, for r = rho 2^d, every injective r-tuple x, the proportion of palindrome-Benes coin outcomes whose density exponent exceeds r(H(rho)+entropy correction(rho)+epsilon) is at most exp(-c r), where H is a supremum over admissible cycle-length laws and allocations defined in the source. (4) Sparse contact: there are positive constants such that, for d at least 1 and 1 <= k < 2^d, the squared sweep-operator norm is at most min(1,(C d k/2^d)^(k/2)), the operator is zero when k=1, and the squared norm is also at most C^k (1+d)^(Ck) (k/2^d)^(k/2). (5) Harmonic: there exist positive constants (with 0<delta<1) and a positive integer p0 such that, for k>0, the norm W of K is at most exp(-c L), at most exp(CL) f^(-zeta) with f the dimension of the Specht module of the tail diagram (mu with its first row removed), and at most exp(-c1 L) D^(-c2); the sweep operator norm is at most exp(-cTail(L+log f)); and for each tuple length k with 1<=k<=2^d, the reflected tuple kernel has (1+delta)-moment bounded by exp(C times level scale) and its p0-th power trace bounded by exp(C times level scale). (6) Smoothing: there is an integer u>=1 and constant C such that the u-th power of every reflected sweep kernel on injective l-tuples has entries at most exp(Cl) divided by the falling factorial of 2^d, and the trace of the u-th power of the full-length kernel is at most exp(C 2^d). (7) Tail: for some p in (1,2] satisfying a density condition (L^p moment bounds of normalized kernel rows and columns by exp(C l)) and some C, the squared sweep-operator norm is at most exp(C k) times the dimension of the tail diagram's Specht module raised to -(p-1)/p. (8) High tail: for positive b, delta, C and some J0, the exponential moment 2^(b*cost) of the palindrome cost above height J-1 has base-2 logarithm at most C k 2^(-bJ) for J>=J0, the full palindrome cost has such moment at most C k (k/2^d)^delta, and a conditional version holds for the split coordinates when 2s<J. (9) Sparse saving: for some C and d0>0, whenever k<2^d and d^(3/4) <= log(2^d/k), the squared sweep norm is at most exp(Ck)(k/2^d)^(k/4), and for d>=d0 at most (k/2^d)^(k/4).

The goal is OAI.ThorpNine.main.

Significance

The central published goal is a conjunction of nine routing and operator estimates. It includes a mixing consequence but also retains the quantitative sparse, dense, and tail regimes needed by the formal package. 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 estimates cover different diagram shapes and occupancy scales. A bound effective for sparse defects can deteriorate in the dense regime, so one uniform estimate cannot simply be substituted for the entire bundle.

Formalization scope

Each conjunct uses its own named MainStatement under the ThorpNine namespaces. The detailed readout below gives its quantifiers and constants. Both forward and reverse sweeps occur, and the package uses complex Specht-module Hilbert spaces.

The shared definitions are supplied by ThorpRouting. 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, Routing densities and representation contraction for Thorp sweeps, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Random coordinate frames allow comparison between different sequences of matching directions in a shuffle. The source uses partially observed card lists to obtain estimates for the full permutation law. The source is OpenAI's September 2026 manuscript.

The companion Conditional information under deterministic coordinate sweeps develops the conditional-information side of the same published eight-clause goal. Both manuscripts are represented by this one draft because they point to the identical formal statement, OAI.ThorpResults.remaining_main.

Setting

A Thorp shuffle acts on $2^d$ binary-labelled positions by independent pair switches followed by a cyclic coordinate rotation. A sweep consists of $d$ physical shuffles. Partial observations record an injective ordered list of card positions.

Formalization targets

$$\sup_\sigma\|q_d^{*32800d}\sigma-U\|_{\mathrm{TV}}\to0,\qquad t_{\mathrm{mix}}(d)=\Theta(\log 2^d).$$

Eight asymptotic results about the Thorp shuffle of 2^d cards, whose positions are the d-bit strings, hold simultaneously. One Thorp step on d≥1 bits uses one fair coin for each (d−1)-bit suffix: the first bit of a position is flipped according to the coin of its remaining bits, and then the bits are cyclically rotated; the d=0 step is the identity. A shuffle of t steps composes t independent such steps, and 'distance' is total variation (half the L¹ distance) from the uniform law on permutations. (1) FrameMain: for every ε>0, for all large d and every starting permutation, the law after 32800·d steps is within total variation ε of uniform. (2) InformationMain has three parts. For large d, any k with 8k≤7·2^d, any start and any list of k distinct labelled positions, the law of the images of the labels after 256·d steps is within ε of uniform on injective k-lists. For large d and 16k≤15·2^d, the same list distance after 1024·d steps is at most (2^d)^(−3/2). Finally, distance(d, 2048·d) tends to 0, and for every d the distance from any start equals distance(d, 2048·d). (3) SpectrumMain: there is p>0 such that for all d≥1 the regularTrace at exponent 2p is at most 17/16 (a sum over Young-diagram shapes of size 2^d of dimension times the trace of |Q|^{2p}, where Q is the averaged Specht-module operator of d-step shuffles) and, for every integer M≥p and every σ, the sweep distance after M·d steps (total variation of the shifted law from uniform) is at most 1/8. (4) SignedMain: for all real η,κ with η>0 there is r≥1 such that, for all d≥1, every shape μ of size 2^d and all Young diagrams α,β,γ with |α|+|β|+|γ|=2^d, the logarithm of the weighted moment dim·Re tr((QQ)^r) is at most a(η,d)·signedEntropy(α,β)+remainderBudget(κ,d,|γ|), where a(η,d)=η(1−1/(2√d)), signedEntropy sums log((|α|+|β|)/rowlength) over cells of α and β, and the remainder is 0 if |γ|=0 and otherwise max(0, a(κ,d)·|γ|·log 2^d−|γ|·log(2^d/|γ|)). (5) DegreeSavingMain: there are an even r≥2 and η>0 such that for all d and shapes μ, dim·Re tr((QQ)^r) ≤ dim^(1−η). (6) FullDensityMain: there is v≥1 such that, for every ε>0 and large d, every shifted law after v·d steps has normalized squared L² density distance (2^d)!·Σ_g(law−1/(2^d)!)² below ε. (7) ForwardMixingMain: there is v≥1 such that for large d every shifted law after v·d steps has total variation below ε. (8) OptimalOrderMain: the mixing time, the least t with distance at most 1/4, is Θ(log 2^d).

The goal is OAI.ThorpResults.remaining_main.

Significance

The selected published goal packages eight results, including fixed-list estimates, spectral moments, signed moments, degree savings, full-density convergence, and optimal-order mixing. The detailed clauses below specify the complete bundle. 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

Changing coordinates must preserve the joint path law, including what has already been revealed. Marginal uniformity of individual cards does not control the full permutation.

Formalization scope

The goal is the shared remaining_main bundle used by several companion manuscripts. It retains all eight formal clauses rather than claiming a new manuscript-specific statement. The displayed bounds are two of those clauses; the full conjunction remains the proof obligation.

The shared definitions are supplied by ThorpRemaining. 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, Random coordinate frames and partial permutation laws, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.
• OpenAI, Conditional information under deterministic coordinate sweeps, preprint, September 2026. Companion manuscript.

Motivation: a dimension saving for the binary coordinate sweep

The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On $N=2^d$ cards, removing the deterministic rotation of coordinates turns $d$ physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability $1/2$. After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.

By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving $\|K_\lambda\|_{\rm op}\le D_\lambda^{-g}$ for the sweep in every irreducible representation $\lambda$ of $S_N$. The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.

Timeline

• 1973 — Thorp introduces the shuffle in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 1981 — Diaconis and Shahshahani introduce the Fourier upper-bound method for random walks on $S_n$ (Z. Wahrsch. 1981).
• 2005/2008 — Morris proves $O(d^{44})$ physical shuffles for $N=2^d$ with a chameleon process that conditions on the trajectory of an occupied set (SIAM J. Comput. 2008); Montenegro and Tetali sharpen it to $O(d^{29})$ (2006).
• 2009 — Morris proves $O((\log N)^4)$ for every even $N$ (Ann. Probab. 2009); Morris, Rogaway and Stegers analyze selected-card Thorp marginals for small-domain encryption (CRYPTO 2009).
• 2012 — Hoang, Morris and Rogaway use a conditional squared-discrepancy calculation for the swap-or-not shuffle (CRYPTO 2012).
• 2013 — Morris proves $O(d^3)$ for $N=2^d$, exposing complete labeled trajectories successively (CPC 2013).
• 2014–2015 — Czumaj and Vöcking: nearly uniform joint positions of a $(1-\varepsilon)$ fraction of the cards after $O(d^2)$ shuffles (ICALP 2014); Czumaj, switching networks (STOC 2015).
• 2026 — The OpenAI preprint Conditional coordinate sweeps and analytic transfer (OpenAI Math Release, September 26, 2026) proves the binary sweep contraction below, giving $t_{\rm mix}(d)=\Theta(d)$ physical shuffles. The preprint has not been peer reviewed and its results are not formally verified.

Setting

Positions are binary strings $\{0,1\}^d$, $N=2^d$ (Lean: Slot d := Fin d → Bool). For a coordinate $j$, a layer flips bit $j$ of a position $x$ according to a fair coin attached to the edge $\{x,x+e_j\}$; the binary sweep applies the layers for $j=1,\dots,d$ in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on $S_N$). For an irreducible unitary representation $\rho_\lambda$ of $S_N$ of dimension $D_\lambda$, the sweep operator is

$$K_\lambda=\mathbb E_{g\sim B_N}\rho_\lambda(g).$$

Write $B_N^{*w}$ for the law of $w$ independent sweeps and $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

For the conditional estimate, an ordered product grid is $\Omega=\Omega_1\times\dots\times\Omega_b$ with each $|\Omega_j|=m_j$ a power of two in $[R,R^2]$; a sweep permutes the lines parallel to coordinate $1$, then coordinate $2$, and so on, each line independently with law $L_m(z)=(1-z)U_m+zB_m$. A family $\mathcal H$ of $h$ prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the $s-h$ free slots has average $K^{\mathcal H}_\lambda$ in each irreducible $\lambda\vdash s-h$, with line cost $C(\mathcal H)=\sum_{L}\log\bigl(|L|^{h_L}/(|L|)_{h_L}\bigr)$.

Formalization targets

Milestone: conditional sweep moment estimate (Theorem 3.1)

There are a power of two $R\ge2$, an integer $q\ge1$ and $z_*>0$ such that for every grid, every feasible family $\mathcal H$, every $z\in[0,z_*]$ and every irreducible $\lambda\vdash s-h$,

$$\log\|K^{\mathcal H}_\lambda\|_{2q}^{2q}\le -c(s)\log D_\lambda+e(s)\,h\log s-C(\mathcal H),$$

with $c(s)=c_0+1/\sqrt{\log s}$, $e(s)=e_0-1/\sqrt{\log s}$, $c_0=e_0=10^{-4}$, and $\log 0=-\infty$.

Goal: binary sweep contraction (Theorem 1.1)

There are absolute constants $g>0$ and $d_0$ such that for all $d\ge d_0$ and every irreducible unitary representation of $S_{2^d}$ of dimension $D$,

$$\|K_\lambda\|_{\rm op}\le D^{-g};$$

the sign representation is annihilated, $\sum_g B_N(g)\,\mathrm{sgn}(g)=0$; and there is an absolute integer $w$ such that

$$\sup_{\tau\in S_N}\bigl\|B_N^{*w}(\cdot\,\tau^{-1})-U_N\bigr\|_{\rm TV}\xrightarrow[d\to\infty]{}0 .$$

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one binary sweep is exactly $d$ physical shuffles, the goal gives $O(d)$ physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: $t$ shuffles reach at most $2^{tN/2}$ permutations) gives the matching lower bound $2d-O(1)$; thus $t_{\rm mix}(d)=\Theta(d)$, improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.

Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on $\mathbb C^D$), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.

Difficulty

The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost $C(\mathcal H)$, which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ($z$ small), while the Thorp sweep is the binary case $z=1$; for a fixed grid the sweep operator is a matrix polynomial in $z$ whose behavior at $z=1$ is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.

Formalization scope

• Goal (binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: $\exists g>0\ \exists d_0\ \forall d\ge d_0\ \forall D$ and every irreducible representation $\rho$ of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of $\sum_g \mathrm{binaryLaw}(g)\rho(g)$ is at most $D^{-g}$ (real power). Sign: for every $d>0$, $\sum_g \mathrm{binaryLaw}(g)\,\mathrm{sgn}(g)=0$. UniformSweepMixingTarget: $\exists w\ \forall\varepsilon>0\ \exists d_0\ \forall d\ge d_0\ \forall\tau$, total variation of the $w$-fold convolution power translated by $\tau$ from uniform is at most $\varepsilon$. Physical shuffles are not modelled; the statement is about sweeps.
• Milestone (conditional_main): grids are Grid with $b\ge1$ coordinates of $r\le\text{bits}_j\le2r$ ($R=2^r$); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is $\mathrm{Re}\operatorname{Tr}((K^*K)^q)$; $z_*\le1/2$.
• The mapped item all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.
• Infrastructure: Specht-module dimension estimates, branching and Pieri rules, signed Schur–Weyl decompositions, Schatten norms, and the subharmonic maximum principle; the analytic-transfer step is reusable for other families of averaging operators polynomial in a parameter.

Selected references

• 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
• 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
• B. Morris, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• 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
• B. Morris, P. Rogaway and T. Stegers, How to encipher messages on a small domain, CRYPTO 2009, LNCS 5677, 286–302. https://doi.org/10.1007/978-3-642-03356-8_17
• V. T. Hoang, B. Morris and P. Rogaway, An enciphering scheme based on a card shuffle, CRYPTO 2012, LNCS 7417, 1–13. https://doi.org/10.1007/978-3-642-32009-5_1
• 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
• A. Berele and A. Regev, Hook Young diagrams, combinatorics and representations of Lie superalgebras, Bull. Amer. Math. Soc. (N.S.) 8 (1983), 337–339. https://doi.org/10.1090/S0273-0979-1983-15110-8
• OpenAI, Conditional coordinate sweeps and analytic transfer, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 2; Theorem 3.1, p. 7). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Conditional-coordinate-sweeps-and-analytic-transfer-September-26-2026/main.pdf

Motivation: optimal-order mixing for the Thorp shuffle

The Thorp shuffle is a simple card-shuffling rule: cut a deck of $n$ cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For $n=2^d$ every individual card is uniform after $d$ shuffles, but the joint order of all $n$ cards is much harder to control. Determining whether $O(d)=O(\log n)$ shuffles suffice to make the full permutation close to uniform was a long-standing question.

Timeline

• 1973 — Thorp introduces the model in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 2005/2008 — Morris proves the first polynomial-in-$d$ bound, $O(d^{44})$ shuffles for $n=2^d$, using evolving sets and a chameleon process (Morris, SIAM J. Comput. 2008).
• 2006 — Montenegro and Tetali sharpen this to $O(d^{29})$ by spectral-profile and evolving-set estimates (Montenegro–Tetali 2006, §6.4).
• 2009 — Morris introduces an entropy method based on card interactions and obtains $O(\log^4 n)$ for every even deck size (Morris, Ann. Probab. 2009).
• 2013 — Morris obtains $O(d^3)$ for dyadic decks (Morris, CPC 2013).
• 2026 — The OpenAI preprint Random-subspace tests and trace smoothing for coordinate sweeps (OpenAI Math Release, September 26, 2026) claims a uniform bound on a fixed Schatten moment of one coordinate sweep in the full regular representation, which yields total-variation mixing after an absolute number of sweeps, i.e. $O(d)$ physical shuffles. The preprint has not been peer reviewed and its result is not formally verified.

Setting

Index the $n=2^d$ positions by binary strings $x\in\mathbb F_2^d$ (in Lean, Card d := Fin d → Bool). One physical shuffle sends

$$(x_1,x_2,\dots,x_d)\longmapsto(x_2,\dots,x_d,\;x_1+\xi_{x_2,\dots,x_d})$$

with independent fair bits $\xi$ (Lean: step d ξ = rotate * pairSwitch ξ). After $d$ physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write $\mu_t$ for the law on $S_n$ of $t$ physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).

For a partition $\lambda\vdash n$ let $V_\lambda$ be the Specht module (the irreducible representation of $S_n$ indexed by $\lambda$), of dimension $D_\lambda$, and let $Q_n(\lambda)=\sum_g \mu_d(g)\,\lambda(g)$ be the average of the sweep in $V_\lambda$. For an operator $Y$, $|Y|=(Y^*Y)^{1/2}$ and traces are unnormalized. The regular trace of the $P$-th power is

$$\operatorname{Tr}_{\rm reg}|Q_n|^P=\sum_{\lambda\vdash n}D_\lambda\operatorname{Tr}_{V_\lambda}|Q_n(\lambda)|^P ,$$

in which the trivial representation contributes exactly $1$. Total variation is $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

Formalization targets

Goal: regular-trace smoothing (Theorem 1.1)

There is an absolute real $P\ge2$ such that for every $d\ge1$ (so $n=2^d\ge2$)

$$\operatorname{Tr}_{\rm reg}|Q_n|^P\le 1+n^{-10},$$

and for every integer $v$ with $2v\ge P$ and every initial deck $\sigma$,

$$\tfrac12\sum_{g\in S_n}\Bigl|\mu_{vd}(g\sigma^{-1})-\tfrac1{n!}\Bigr|\le\tfrac12\,n^{-5}.$$

The constant $P$ is not specified; only its existence and uniformity in $d$ are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one sweep is $d$ physical shuffles, the second clause shows that $O(d)=O(\log n)$ Thorp shuffles bring the full permutation within $\tfrac12 n^{-5}$ of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least $2d-O(1)$ physical shuffles are needed, so this order is optimal, improving the $O(d^3)$ bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.

Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each $d$. A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.

Difficulty

Single-card and few-card statistics mix after one sweep, but the full permutation involves all $\sim n\log n$ bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of $Q_n(\lambda)$ separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension $D_\lambda$, and the number of partitions grows like $e^{c\sqrt n}$. A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to $\sqrt{n!}$, and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.

Formalization scope

• Positions are Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of $2^d$ are Young diagrams of cardinality $2^d$ (Shapes (2^d)).
• The Specht module is built concretely as the span of the orbit of the standard polytabloid in the space of functions on tabloids, transported to a Euclidean (Hilbert) space; cards are relabelled to cells by a fixed bijection. Q d μ is the average over all coin sequences of length $d$ of the representation of run d d.
• absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. $\operatorname{Tr}|A|^P$; regularTrace multiplies by finrank.
• sweepDistance d v σ is total variation of the law of $v\cdot d$ physical shuffles, right-translated by $\sigma$, from the uniform weight $1/(2^d)!$. The integer $v$ is converted with Int.toNat; since $P\ge2$ and $2v\ge P$, $v\ge1$ and no truncation occurs.
• The support lower bound (Proposition 5.1) is not part of the goal.
• Infrastructure needed: Specht-module dimensions and branching, Schatten-norm inequalities (Hölder, Araki–Lieb–Thirring), Schur–Weyl duality, and the partial-deck density bound from the companion preprint on routing densities. Contributions formalizing any of these pieces are welcome.

Selected references

• 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, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• 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
• H. Araki, On an inequality of Lieb and Thirring, Lett. Math. Phys. 19 (1990), 167–170. https://doi.org/10.1007/BF01045887
• A. Berele and A. Regev, Hook Young diagrams with applications to combinatorics and to representations of Lie superalgebras, Adv. Math. 64 (1987), 118–175. https://doi.org/10.1016/0001-8708(87)90007-7
• B. E. Sagan, The Symmetric Group, 2nd ed., GTM 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
• OpenAI, Random-subspace tests and trace smoothing for coordinate sweeps, OpenAI Math Release preprint, September 26, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Random-subspace-tests-and-trace-smoothing-for-coordinate-sweeps-September-26-2026/paper.pdf

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: tensor squares that contain everything

The irreducible complex representations of the symmetric group $S_n$ are indexed by partitions $\lambda\vdash n$ and written $S^\lambda$ (Specht modules). Decomposing a tensor product $S^\lambda\otimes S^\mu$ (with the diagonal action) into irreducibles is governed by the Kronecker coefficients

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

which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.

Timeline

• 2012 — Saxl proposes (UCLA Combinatorics Seminar, 20 March 2012) that the staircase $\rho_m=(m,m-1,\dots,1)$ at triangular degree $n=m(m+1)/2$ has this property; recorded by Pak, Panova and Vallejo.
• 2013 — Heide, Saxl, Tiep and Zalesski conjecture an analogous covering property for alternating simple groups (HSTZ 2013, Rem. 1.3(3)).
• 2013/2016 — Pak, Panova and Vallejo state the tensor square conjecture for $n\ge3$, $n\ne4,9$, and the Saxl conjecture, and give a character-nonvanishing criterion (PPV 2016, Conj. 1.1–1.2, Lemma 1.3).
• 2015 — Ikenmeyer proves the staircase assertion for all $\nu$ comparable with the staircase in dominance order (Ikenmeyer 2015, Thm 2.1).
• 2017 — Luo and Sellke: staircase squares contain almost all partitions, and fourth powers cover everything in large degree (Luo–Sellke 2017).
• 2018 — Bessenrodt: all double-hook constituents (Bessenrodt 2018, Thm 4.10).
• 2021 — Li: the triple-hook case, and a conjectured family for nontriangular degrees (Li 2021).
• 2023 — Harman and Ryba: staircase tensor cubes contain everything (Harman–Ryba 2023, Thm 1.1).
• 2026 — An OpenAI preprint, Universal Tensor Squares for Symmetric Groups (OpenAI Math Release, September 24, 2026), claims the tensor square conjecture for every $n\notin\{2,4,9\}$, building on a companion preprint that proves Saxl's conjecture in a cyclic form. Neither preprint is peer reviewed and the main theorem is not formally verified; its proof uses exact computer calculations for degrees up to $64$.

Setting

For a Young diagram $\lambda$ with $n$ cells, fix a bijection $t$ between $\{0,\dots,n-1\}$ and the cells (a tableau). The Lean development realizes $S^\lambda$ inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ($d$ = number of rows), with $S_n$ acting by permuting letters: the polytabloid $e_t$ is the signed sum, over the column group of $t$, of the permuted indicator of the row word of $t$, and Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The Kronecker coefficient kronecker a b t is finrank of the space of $S_n$-intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape $\lambda$.

Formalization targets

Goal: a universal tensor square in every degree $n\notin\{2,4,9\}$

For every positive integer $n$ with $n\ne2,4,9$ there is a partition $\lambda\vdash n$ such that

$$g(\lambda,\lambda,\nu)>0\qquad\text{for every }\nu\vdash n ,$$

so the tensor square $S^\lambda\otimes S^\lambda$ contains every irreducible representation of $S_n$. The Lean statement asserts, for one Young diagram $\lambda$ with $n$ cells: positivity of kronecker for every target diagram $\nu$ with $n$ cells; irreducibility of spechtRep for $\lambda$; and that every finite-dimensional irreducible complex representation of $S_n$ admits an injective intertwining map into $S^\lambda\otimes S^\lambda$. This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.

Significance

The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen $\lambda$ must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of $\mathrm{GL}_n(\mathbb F_q)$ that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.

Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible $n\le64$, and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.

Difficulty

Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and $n=2,4,9$ are genuine exceptions.

Formalization scope

• Partitions are Mathlib YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of $S^\nu$ in the tensor square.
• The third conjunct quantifies over all finite-dimensional complex irreducible representations in a fixed universe; proving it requires that every irreducible of $S_n$ is isomorphic to some Specht module. The second conjunct (irreducibility of $S^\lambda$) is a standard fact the source uses implicitly.
• $n>0$ and $n\ne2,4,9$ match the source; $n=1$ is trivial.
• Needed infrastructure: Specht module theory (irreducibility, completeness), characters and Murnaghan–Nakayama, Littlewood–Richardson branching, verified computation for $n\le 64$. The Specht and Kronecker layer is shared with the companion Saxl 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
• 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
• 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, Tensor products of unipotent characters of general linear groups over finite fields, Transform. Groups 18 (2013), 233–262. https://doi.org/10.1007/s00031-013-9211-3
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf
• OpenAI, Universal Tensor Squares for Symmetric Groups, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf

Motivation

Let $A$ be a finite-dimensional algebra over a field. A finite-dimensional module $M$ is self-orthogonal if $\operatorname{Ext}^i_A(M,M)=0$ for every $i>0$. Tachikawa's second conjecture asserts that over a self-injective algebra every self-orthogonal module is projective. It belongs to the cluster of homological conjectures around quasi-Frobenius algebras and dominant dimension recorded in Tachikawa's 1973 monograph, alongside the Nakayama, generalized Nakayama and Auslander–Reiten conjectures. Since $\operatorname{Ext}^i_A(M,A)=0$ automatically when $A$ is self-injective, it is exactly the self-injective case of the Auslander–Reiten conjecture. Enomoto and Marczinzik showed that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture, so the two were expected to stand or fall together.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a counterexample over a symmetric algebra. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

• 1975 — Auslander and Reiten formulate the conjecture in their work on the generalized Nakayama conjecture (Proc. AMS 1975).
• 1993 — Auslander, Ding and Solberg prove it for complete local complete intersections (J. Algebra 1993).
• 1994–1995 — Schulz constructs a nonprojective module without self-extensions over a ring outside the Artin-algebra setting (Arch. Math. 1994) and quantum-exterior-algebra modules with eventually vanishing self-extensions (J. Aust. Math. Soc. 1995).
• 2004 — Huneke and Leuschke prove the conjecture for excellent Cohen–Macaulay normal domains containing $\mathbb Q$ (J. Algebra 2004); Huneke, Şega and Vraciu treat commutative Artinian local rings with radical cube zero (Illinois J. Math. 2004).
• 2008 — Luo and Huang record the Gorenstein-projective variant (J. Algebra 2008).
• 2010 — Christensen and Holm show that rings satisfying Auslander's condition satisfy the conjecture (Math. Z. 2010).
• 2017–2022 — Erdmann's analysis of weakly symmetric algebras with $J^3=0$ (J. Aust. Math. Soc. 2017); Ringel and Zhang on short local algebras (J. LMS 2022).
• 2026 — Zhang and Zhou prove the conjecture for split algebras with radical cube zero (arXiv:2609.08679) and for Igusa–Todorov algebras (arXiv:2609.14453); Xia for quantum complete intersections (arXiv:2609.24007); Enomoto shows that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture (arXiv:2609.19172).
• September 2026 — Two OpenAI preprints claim counterexamples: an explicit eight-simple Gorenstein-projective example (source) and a symmetric-algebra counterexample to Tachikawa's second conjecture (source).

Setting

Let $k=\mathbb F_2(q,H_1,H_2)$ be the rational function field in three algebraically independent variables. Write $D=\operatorname{Hom}_k(-,k)$. A finite-dimensional $k$-algebra $A$ is symmetric if $A\cong DA$ as $A$-bimodules, where $(a\cdot f\cdot b)(c)=f(bca)$; equivalently there is a $k$-linear isomorphism $e:A\to DA$ with $e(ab)(c)=e(b)(ca)=e(a)(bc)$. Symmetric algebras are self-injective. For a finite-dimensional left $A$-module $M$, $\operatorname{Ext}^i_A(M,M)$ is computed in the category of left $A$-modules.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There exist a finite-dimensional associative unital symmetric $k$-algebra $A$ and a finite-dimensional unital left $A$-module $M$ such that $M$ is not projective and

$$\operatorname{Ext}^i_A(M,M)=0\qquad\text{for every integer }i>0.$$

In particular Tachikawa's second conjecture is false, and since $A$ is self-injective the same pair is a symmetric counterexample to the Auslander–Reiten conjecture.

Significance

The result itself. The theorem disproves Tachikawa's second conjecture in the strongest natural class (symmetric algebras). Through an associated endomorphism algebra, the preprint further claims counterexamples to the classical, generalized and strong Nakayama conjectures, the Auslander–Gorenstein conjecture and the Wakamatsu tilting conjecture, persisting under every field extension (Corollary 1.2, p. 4), together with consequences for finitistic dimensions (Corollary 1.3, p. 5). Those corollaries are not part of this mission's goal. A companion preprint gives an explicit eight-simple triangular counterexample to the Auslander–Reiten conjecture.

Formalizing it. The statement uses only notions already in Mathlib (finite-dimensional algebras, projective modules, Abelian.Ext in ModuleCat), so it is a clean target. The proof needs trivial extensions $\Lambda\ltimes D\Lambda$, totally acyclic complexes, stable categories of symmetric algebras, Koszul computations of $\operatorname{Ext}$-algebras, and Hochschild bar complexes; these are reusable throughout representation theory.

Difficulty

Known non-examples come close but fail: Schulz's quantum exterior modules have vanishing higher self-extensions but nonzero $\operatorname{Ext}^1$; Böhmler and Marczinzik have a commutative self-injective example with only $\operatorname{Ext}^1=\operatorname{Ext}^2=0$. Vanishing in every positive degree requires controlling an infinite resolution. In the preprint, the passage to a symmetric algebra also requires vanishing of the negative part of a complete self-extension complex (condition (1.1), p. 2), which is what the transfer through the trivial extension $A=\Lambda\ltimes D\Lambda$, $M=A\otimes_\Lambda Z$ (Proposition 3.2, p. 12) consumes. Producing it needs two twists $H_1,H_2$ acting by distinct scalars on every nonzero homogeneous self-map space, and genuine bimodule lifts of stable maps (Proposition 6.1, p. 21).

Formalization scope

• The field is FractionRing (MvPolynomial (Fin 3) (ZMod 2)), i.e. $\mathbb F_2(q,H_1,H_2)$ with independent variables.
• SymmetricOver k A asks for a $k$-linear equivalence e : A ≃ₗ[k] Module.Dual k A with e (a*b) c = e b (c*a) and e (a*b) c = e a (b*c), i.e. a bimodule isomorphism $A\cong DA$.
• Counterexample asserts existence of A : Type with Ring and Algebra k structures, Module.Finite k A, symmetric; and M with compatible Module A, Module k (IsScalarTower), Module.Finite k M, ¬ Module.Projective A M, and Subsingleton (Abelian.Ext (ModuleCat.of A M) (ModuleCat.of A M) n) for all n > 0.
• The nonprojectivity clause rules out $M=0$ and semisimple $A$, so the statement is not trivially satisfiable.

Selected references

• OpenAI, A counterexample to Tachikawa's second conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-counterexample-to-Tachikawas-second-conjecture-September-23-2026/paper.pdf
• OpenAI, An explicit counterexample to the Auslander–Reiten conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf
• H. Tachikawa, Quasi-Frobenius Rings and Generalizations, Lecture Notes in Mathematics 351, Springer, 1973.
• K. Diveris, M. Purin, Vanishing of self-extensions over symmetric algebras, J. Pure Appl. Algebra (2014). https://doi.org/10.1016/j.jpaa.2013.10.012
• K. Erdmann, Ext-finite modules for weakly symmetric algebras with radical cube zero, J. Aust. Math. Soc. (2017). https://doi.org/10.1017/S1446788716000331
• M. Auslander, I. Reiten, On a generalized version of the Nakayama conjecture, Proc. Amer. Math. Soc. 52 (1975). https://doi.org/10.1090/S0002-9939-1975-0389977-6
• M. Auslander, S. Ding, Ø. Solberg, Liftings and weak liftings of modules, J. Algebra (1993). https://doi.org/10.1006/jabr.1993.1076
• C. Huneke, G. J. Leuschke, On a conjecture of Auslander and Reiten, J. Algebra (2004). https://doi.org/10.1016/j.jalgebra.2003.07.018
• L. W. Christensen, H. Holm, Algebras that satisfy Auslander's condition on vanishing of cohomology, Math. Z. (2010). https://doi.org/10.1007/s00209-009-0500-4
• R. Luo, Z. Huang, When are torsionless modules projective?, J. Algebra (2008). https://doi.org/10.1016/j.jalgebra.2008.04.027
• R. Schulz, A non-projective module without self-extensions, Arch. Math. (1994). https://doi.org/10.1007/BF01193735
• H. Enomoto, Tachikawa's second conjecture implies the Auslander–Reiten conjecture, arXiv:2609.19172 (2026). https://arxiv.org/abs/2609.19172v1
• X. Zhang, P. Zhou, The Auslander–Reiten conjecture for algebras with radical cube zero, arXiv:2609.08679 (2026). https://arxiv.org/abs/2609.08679v1

Motivation

In the representation theory of finite-dimensional algebras, vanishing of $\operatorname{Ext}$ groups is the standard way of detecting projectivity homologically. The Auslander–Reiten conjecture (1975) asserts that a finitely generated module $M$ over an Artin algebra $R$ is projective as soon as

$$\operatorname{Ext}^i_R(M,M\oplus R)=0\qquad\text{for every }i>0.$$

It arose from Auslander and Reiten's work on the generalized Nakayama conjecture and sits in a web of homological conjectures (Nakayama, Tachikawa, Gorenstein-projective, Auslander–Gorenstein) that were long expected to hold. A module is Gorenstein-projective if it is a cokernel in a doubly infinite exact complex of finitely generated projectives that stays exact under $\operatorname{Hom}_R(-,R)$; the Gorenstein-projective conjecture is the restriction of the Auslander–Reiten conjecture to such modules.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims an explicit counterexample to both conjectures. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

• 1975 — Auslander and Reiten formulate the conjecture in their work on the generalized Nakayama conjecture (Proc. AMS 1975).
• 1993 — Auslander, Ding and Solberg prove it for complete local complete intersections (J. Algebra 1993).
• 1994–1995 — Schulz constructs a nonprojective module without self-extensions over a ring outside the Artin-algebra setting (Arch. Math. 1994) and quantum-exterior-algebra modules with eventually vanishing self-extensions (J. Aust. Math. Soc. 1995).
• 2004 — Huneke and Leuschke prove the conjecture for excellent Cohen–Macaulay normal domains containing $\mathbb Q$ (J. Algebra 2004); Huneke, Şega and Vraciu treat commutative Artinian local rings with radical cube zero (Illinois J. Math. 2004).
• 2008 — Luo and Huang record the Gorenstein-projective variant (J. Algebra 2008).
• 2010 — Christensen and Holm show that rings satisfying Auslander's condition satisfy the conjecture (Math. Z. 2010).
• 2017–2022 — Erdmann's analysis of weakly symmetric algebras with $J^3=0$ (J. Aust. Math. Soc. 2017); Ringel and Zhang on short local algebras (J. LMS 2022).
• 2026 — Zhang and Zhou prove the conjecture for split algebras with radical cube zero (arXiv:2609.08679) and for Igusa–Todorov algebras (arXiv:2609.14453); Xia for quantum complete intersections (arXiv:2609.24007); Enomoto shows that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture (arXiv:2609.19172).
• September 2026 — Two OpenAI preprints claim counterexamples: an explicit eight-simple Gorenstein-projective example (source) and a symmetric-algebra counterexample to Tachikawa's second conjecture (source).

Setting

Let $k=\mathbb F_2(q,H_1,H_2)$ be the field of rational functions in three algebraically independent variables over $\mathbb F_2$. A finite-dimensional $k$-algebra $\Lambda$ is an Artin algebra. For a left $\Lambda$-module $Z$, $\operatorname{Ext}^i_\Lambda(Z,-)$ is computed in the abelian category of left $\Lambda$-modules. $\operatorname{rad}\Lambda$ denotes the Jacobson radical. $Z$ is Gorenstein-projective when $Z\cong\operatorname{coker}(P_1\to P_0)$ for an exact complex $(P_i)_{i\in\mathbb Z}$ of finitely generated projective modules such that every map $P_i\to Q$ into a projective $Q$ that vanishes on the image of $P_{i+1}$ factors through $P_i\to P_{i-1}$. For a field extension $K/k$, write $\Lambda_K=K\otimes_k\Lambda$ and $Z_K=K\otimes_kZ$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist a finite-dimensional $k$-algebra $\Lambda$ and a finite-dimensional nonprojective left $\Lambda$-module $Z$ such that

$$\operatorname{Ext}^i_\Lambda(Z,Z)=0=\operatorname{Ext}^i_\Lambda(Z,\Lambda)\qquad(i\ge1),$$

$Z$ is Gorenstein-projective, $\Lambda/\operatorname{rad}\Lambda\cong k^8$ as $k$-algebras, and $(\operatorname{rad}\Lambda)^4\ne0$. All of these conclusions hold again for $\Lambda_K$ and $Z_K$ for every field extension $K/k$.

Significance

The result itself. The theorem refutes the Auslander–Reiten conjecture for Artin algebras and the Gorenstein-projective conjecture; by extending scalars to an algebraic closure it also refutes them over an algebraically closed field of characteristic two. Since $Z\oplus\Lambda$ is then a nonprojective generator with no positive self-extensions, the generator formulation fails too. The structural data ($8$ simple modules, split, $\operatorname{rad}^4\ne0$) place the example just outside the radical-cube-zero class where the conjecture is now known. The commutative case is not resolved.

Formalizing it. A formal proof would require Ext in module categories (available in Mathlib via Abelian.Ext), complete resolutions, triangular matrix algebras, trivial extensions and Hochschild cocycles, and base change of Ext under field extension. The counterexample is concrete, so much of the verification reduces to finite linear algebra over $k$ plus an infinite periodic-type resolution with uniform kernel formulas.

Difficulty

All positive results exploit some finiteness or rigidity (complete intersections, Cohen–Macaulay domains, radical cube zero, Auslander's condition), and the natural candidates for counterexamples (Schulz's quantum exterior algebra modules) have self-extensions that only vanish eventually, with $\operatorname{Ext}^1\ne0$. Vanishing in every positive degree, simultaneously against $Z$ and $\Lambda$, is the hard requirement. The preprint (Section 1.2, pp. 3–4) converts a suitable stable map over a symmetric algebra into a module over a triangular algebra $\Lambda=\begin{pmatrix}A&0\\F&A\end{pmatrix}$ (Proposition 3.1, p. 6), uses powers of $q$ for a resolution with uniform kernels, and kills every positive self-extension with two independent twists $H_1,H_2$, using that $H_1/H_2$ has infinite multiplicative order.

Formalization scope

• The field is FractionRing (MvPolynomial (Fin 3) (ZMod 2)), and the goal also asserts that the three generators are algebraically independent over $\mathbb F_2$.
• The algebra and module are packaged as a System (types in Type, with Ring, Algebra K, Module, and IsScalarTower K Λ Z instances). Conclusions asserts finite dimensionality over $k$, ¬ Module.Projective Λ Z, the totally acyclic witness, Subsingleton of Abelian.Ext in ModuleCat for all $i>0$ against $Z$ and against $\Lambda$, a $k$-algebra isomorphism $\Lambda/\operatorname{Jac}(\Lambda)\cong k^8$, and $\operatorname{Jac}(\Lambda)^4\ne\bot$.
• Field extension is quantified over every field E with Algebra K E in an arbitrary universe; the module structure on $E\otimes_k Z$ must satisfy $(a\otimes r)(b\otimes z)=ab\otimes rz$, which pins it to the standard one.
• The totally acyclic condition tests exactness of $\operatorname{Hom}(-,Q)$ for all projective $Q$, which for complexes of finitely generated projectives is equivalent to the source's $\operatorname{Hom}(-,\Lambda)$ condition.
• No trivialization: nonprojectivity and $\operatorname{rad}^4\ne0$ exclude the zero and semisimple cases.

Selected references

• OpenAI, An explicit counterexample to the Auslander–Reiten conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf
• OpenAI, A counterexample to Tachikawa's second conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-counterexample-to-Tachikawas-second-conjecture-September-23-2026/paper.pdf
• M. Auslander, I. Reiten, On a generalized version of the Nakayama conjecture, Proc. Amer. Math. Soc. 52 (1975). https://doi.org/10.1090/S0002-9939-1975-0389977-6
• M. Auslander, S. Ding, Ø. Solberg, Liftings and weak liftings of modules, J. Algebra (1993). https://doi.org/10.1006/jabr.1993.1076
• C. Huneke, G. J. Leuschke, On a conjecture of Auslander and Reiten, J. Algebra (2004). https://doi.org/10.1016/j.jalgebra.2003.07.018
• L. W. Christensen, H. Holm, Algebras that satisfy Auslander's condition on vanishing of cohomology, Math. Z. (2010). https://doi.org/10.1007/s00209-009-0500-4
• R. Luo, Z. Huang, When are torsionless modules projective?, J. Algebra (2008). https://doi.org/10.1016/j.jalgebra.2008.04.027
• R. Schulz, A non-projective module without self-extensions, Arch. Math. (1994). https://doi.org/10.1007/BF01193735
• H. Enomoto, Tachikawa's second conjecture implies the Auslander–Reiten conjecture, arXiv:2609.19172 (2026). https://arxiv.org/abs/2609.19172v1
• X. Zhang, P. Zhou, The Auslander–Reiten conjecture for algebras with radical cube zero, arXiv:2609.08679 (2026). https://arxiv.org/abs/2609.08679v1

Motivation

Every module over a ring has a projective resolution, and its length, the projective dimension, measures how far the module is from being projective. Over a finite-dimensional algebra, some modules have infinite projective dimension; the finitistic dimension conjectures ask whether, among the modules whose projective dimension is finite, these finite values are bounded. The questions were publicized by Bass in 1960 and became central problems in the representation theory of finite-dimensional algebras, tied to many other homological conjectures (Nakayama, Gorenstein symmetry, Auslander–Reiten), each of which would follow from finiteness of the finitistic dimension.

Timeline

• 1960. Bass publicizes the finitistic-dimension questions (doi:10.1090/S0002-9947-1960-0157984-8).
• 1991. Green, Kirkman and Kuzmanovich prove little finitistic finiteness for finite-dimensional monomial algebras (doi:10.1016/0021-8693(91)90062-D); Green and Huisgen-Zimmermann treat Artin algebras with radical cube zero.
• 1992. Huisgen-Zimmermann constructs monomial algebras whose little and big finitistic dimensions differ ($n$ versus $n+1$), so the two invariants are not equal in general (doi:10.1007/BF02100610).
• 1995. Huisgen-Zimmermann's survey "a tale of 3.5 decades" describes the state of the problems (doi:10.1007/978-94-011-0443-2_41).
• 2005. Igusa and Todorov introduce syzygy invariants and prove finiteness for Artin algebras of representation dimension at most three.
• 2019. Rickard shows that if injective modules generate the unbounded derived category, then the big finitistic dimension is finite (doi:10.1016/j.aim.2019.106735).
• 2024. Cummings proves that universal little finitistic finiteness is equivalent to its left–right symmetry (doi:10.1112/blms.12954).

The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample to the little finitistic-dimension conjecture over $\mathbb C$. A companion OpenAI preprint independently gives a characteristic-two example.

Setting

Let $A$ be a finite-dimensional unital algebra over $\mathbb C$. For a left $A$-module $N$, $\operatorname{pd}_AN\in\{0,1,2,\dots\}\cup\{\infty\}$ is the minimal length of a projective resolution. The little finitistic dimension is

$$\operatorname{findim}A=\sup\{\operatorname{pd}_AN:\ N\ \text{finitely generated left } A\text{-module},\ \operatorname{pd}_AN<\infty\},$$

and the big finitistic dimension $\operatorname{Findim}A$ is the same supremum over all left modules. Over a finite-dimensional algebra, finitely generated and finite-dimensional modules coincide. The little finitistic-dimension conjecture asserts $\operatorname{findim}A<\infty$ for every such $A$.

Injective left modules generate if the smallest triangulated subcategory of the unbounded derived category of left modules that contains them and is closed under arbitrary coproducts is the whole category.

Formalization targets

Goal: Theorem 1.1

$$\exists\ A\ \text{finite-dimensional over } \mathbb C:\quad \forall m\ge1\ \exists N_m\ \text{finitely generated with}\ 2m-2\le\operatorname{pd}_AN_m<\infty;\ \text{hence}\ \operatorname{findim}A=\infty.$$

The Lean statement OAI.LittleFinitistic.Main.exists_counterexample is open on the platform.

Milestone: Corollary 1.2

$$\exists\ \Lambda:\ \operatorname{findim}\Lambda=\operatorname{Findim}\Lambda=\infty,\quad \operatorname{findim}\Lambda^{\rm op}=\operatorname{Findim}\Lambda^{\rm op}=0,$$

injective left $\Lambda$-modules do not generate, and injective right $\Lambda$-modules do.

Significance

Theorem 1.1 refutes the little finitistic-dimension conjecture: a single finite-dimensional algebra has finitely generated modules with terminating projective resolutions of unbounded length. Since $\operatorname{findim}\le\operatorname{Findim}$, it also refutes the big version for Artin algebras, and by Rickard's theorem gives an algebra for which injectives do not generate the derived category. Corollary 1.2 shows that finiteness can fail on one side and hold on the other in the most extreme way, in contrast with Cummings' equivalence of universal finiteness and left–right symmetry.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Because many homological conjectures were known to follow from the finitistic-dimension conjecture, an independent check of a counterexample is of direct interest.

Difficulty

Positive results cover large classes (monomial, radical cube zero, representation dimension at most three), so a counterexample must escape all of them. The finitistic dimension of one fixed algebra must be unbounded, which requires encoding an unbounded family of terminating processes into fixed finite data. The paper realizes a "selection process" from an infinite finitely presented group algebra by a single bounded bimodule complex over a finite-dimensional algebra; making this realization uniform in the input module, and turning it into ordinary projective resolutions over a trivial extension, are the main obstacles.

Formalization scope

• Algebras are A : Type with [Ring A] [Algebra ℂ A] and FiniteDimensional ℂ A; modules are objects of ModuleCat.{0} A, finiteness is Module.Finite A N.
• projectiveDimension is Mathlib's CategoryTheory.projectiveDimension, valued in WithBot ℕ∞, equal to ⊤ for infinite dimension; littleFinitisticDimension and bigFinitisticDimension are suprema over modules of finite projective dimension.
• Right modules are left modules over Aᵐᵒᵖ.
• InjectivesGenerate uses HasDerivedCategory.standard and quantifies over isomorphism-closed triangulated properties closed under coproducts indexed by Type u and containing all injectives in degree 0.

A complete development needs derived tensor products of bimodule complexes, trivial extension algebras $D\ltimes X$ and their bar resolutions, finite presentations of group algebras and their finite-dimensional representations, and (for the milestone) Rickard's theorem and Cummings' triangular algebra. Contributions formalizing Proposition 2.1 (selection), Theorem 4.1 (tensor realization) and Proposition 6.1 (bar splitting) are welcome.

Selected references

• OpenAI, An algebra of infinite little finitistic dimension, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-algebra-of-infinite-little-finitistic-dimension-September-23-2026/paper.pdf
• H. Bass, Finitistic dimension and a homological generalization of semi-primary rings, Trans. Amer. Math. Soc., 1960. https://doi.org/10.1090/S0002-9947-1960-0157984-8
• B. Zimmermann Huisgen, Homological domino effects and the first Finitistic Dimension Conjecture, Invent. Math., 1992. https://doi.org/10.1007/BF02100610
• B. Zimmermann Huisgen, The finitistic dimension conjectures — a tale of 3.5 decades, in Abelian Groups and Modules, 1995. https://doi.org/10.1007/978-94-011-0443-2_41
• E. L. Green, E. E. Kirkman, J. Kuzmanovich, Finitistic dimensions of finite dimensional monomial algebras, J. Algebra, 1991. https://doi.org/10.1016/0021-8693(91)90062-D
• K. Igusa, G. Todorov, On the finitistic global dimension conjecture for Artin algebras, in Representations of Algebras and Related Topics, 2005.
• J. Rickard, Unbounded derived categories and the finitistic dimension conjecture, Adv. Math., 2019. https://doi.org/10.1016/j.aim.2019.106735
• C. Cummings, Left–right symmetry of finite finitistic dimension, Bull. London Math. Soc., 2024. https://doi.org/10.1112/blms.12954

Motivation: the Shareshian–Wachs elementary-positivity conjecture

The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("$e$-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted $e$-positivity for incomparability graphs of $(3+1)$-free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a $q$-graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in $q$ with nonnegative integer coefficients. The $q$-refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.

Timeline

• 1993 — Stanley and Stembridge formulate the $e$-positivity conjecture for $(3+1)$-free posets (J. Combin. Theory Ser. A 1993); Haiman's immanant results imply Schur positivity (JAMS 1993).
• 1995 — Stanley introduces the chromatic symmetric function (Adv. Math. 1995).
• 1996 — Gasharov gives a positive Schur expansion via poset tableaux (Discrete Math. 1996).
• 2012/2016 — Shareshian and Wachs introduce the chromatic quasisymmetric function, prove its symmetry and Schur positivity for natural unit interval graphs, and conjecture elementary positivity over $\mathbb N[q]$ and the Hessenberg connection (Configuration Spaces 2012; Adv. Math. 2016).
• 2013 — Guay-Paquet reduces the Stanley–Stembridge conjecture to unit interval orders (arXiv:1306.2400).
• 2015 — Athanasiadis gives a power-sum expansion (Electron. J. Combin. 2015).
• 2016–2018 — Brosnan–Chow (Adv. Math. 2018) and Guay-Paquet (arXiv:1601.05498) prove the Hessenberg representation identity.
• 2019–2023 — Positivity for substantial subfamilies: abelian Hessenberg varieties (Harada–Precup 2019), explicit expansions (Cho–Huh 2019), melting lollipops (Huh–Nam–Yoo 2020), abelian Dyck paths via $q$-rook theory (Colmenarejo–Morales–Panova 2023); the modular law of Abreu and Nigro (J. Combin. Theory Ser. A 2021).
• 2024–2025 — Hikita proves the Stanley–Stembridge conjecture ($q=1$) via a probabilistic formula (arXiv:2410.12758); his weights do not give coefficientwise positivity in $\mathbb N[q]$. Griffin, Mellit, Romero, Weigl and Wen give an independent proof (arXiv:2504.06936).
• 2026 — The OpenAI preprint Elementary positivity of chromatic quasisymmetric functions (OpenAI Math Release, September 24, 2026) claims elementary positivity over $\mathbb N[q]$ for all natural unit interval graphs, with an explicit permutation witness. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $h:[n]\to[n]$ be weakly increasing with $i\le h(i)$. The natural unit interval graph $G=G(h)$ has vertices $[n]=\{1,\dots,n\}$ and edges $\{i,j\}$ with $i<j\le h(i)$. A proper coloring $f:[n]\to\mathbb N_{>0}$ gives different colors to adjacent vertices, and $\operatorname{asc}_G(f)$ counts edges $\{a<b\}$ with $f(a)<f(b)$. The chromatic quasisymmetric function is

$$\chi_G(X;q)=\sum_{f\ \text{proper}} q^{\operatorname{asc}_G(f)}\prod_{a=1}^n x_{f(a)} .$$

For a partition $\lambda$, $e_\lambda=\prod_i e_{\lambda_i}$ with $e_k=\sum_{i_1<\dots<i_k}x_{i_1}\cdots x_{i_k}$. Let $D^0_G$ be the set of permutations $\sigma$ (as words $\sigma_1\cdots\sigma_n$) such that every adjacent descent $\sigma_i>\sigma_{i+1}$ is an edge, and $\operatorname{ginv}_G(\sigma)$ the number of inversions $i<j$, $\sigma_i>\sigma_j$, with $\{\sigma_i,\sigma_j\}$ an edge.

In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is $\chi_G$ in $r$ variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define $D^0_G$ and $\operatorname{ginv}_G$; a PermutationWitness is a map $\theta:D^0_G\to\{\lambda\vdash n\}$ together with the identity below in every number $r$ of variables, using Mathlib's MvPolynomial.esymmPart.

Formalization targets

Goal: elementary positivity with a permutation witness (Theorem 1.1)

For every $n$ and every natural unit interval graph $G$ on $[n]$ there is a map $\theta_G:D^0_G\to\{\lambda\vdash n\}$ with

$$\chi_G(X;q)=\sum_{\sigma\in D^0_G} q^{\operatorname{ginv}_G(\sigma)}\,e_{\theta_G(\sigma)}(X).$$

In particular every elementary coefficient of $\chi_G$ lies in $\mathbb N[q]$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at $q=1$, via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of $D^0_G$ an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.

Formalizing it. The statement is a finite polynomial identity for each $n$, $G$ and $r$, fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.

Difficulty

The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at $q=1$, and Hikita's probabilistic formula has rational $q$-weights that are only positive at real $q>0$, not coefficientwise. A proof over $\mathbb N[q]$ must produce, for each elementary partition and each power of $q$, a nonnegative integer count, uniformly over all graphs.

Formalization scope

• Graphs are encoded by h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are $i<j\le h(i)$ in either order.
• Colorings use $r$ colors Fin r and the identity is required for every $r\in\mathbb N$, which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree $n$.
• Coefficients live in Polynomial ℕ, so nonnegativity in $\mathbb N[q]$ is built into the statement; the witness theta is an arbitrary function on the finite set $D^0_G$. The source's additional assertion that $\theta_G$ is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.
• Needed infrastructure: symmetric functions in finitely many variables, elementary basis manipulations, and bijections on ordered independent-set collections. These are reusable for other chromatic-function and LLT-positivity problems.

Selected references

• R. P. Stanley and J. R. Stembridge, On immanants of Jacobi–Trudi matrices and permutations with restricted position, J. Combin. Theory Ser. A 62 (1993). https://doi.org/10.1016/0097-3165(93)90048-D
• R. P. Stanley, A symmetric function generalization of the chromatic polynomial of a graph, Adv. Math. 111 (1995), 166–194. https://doi.org/10.1006/aima.1995.1020
• J. Shareshian and M. L. Wachs, Chromatic quasisymmetric functions, Adv. Math. 295 (2016). https://doi.org/10.1016/j.aim.2015.12.018
• M. Guay-Paquet, A modular law for the chromatic symmetric functions of (3+1)-free posets, arXiv:1306.2400 (2013). https://arxiv.org/abs/1306.2400v1
• P. Brosnan and T. Y. Chow, Unit interval orders and the dot action on the cohomology of regular semisimple Hessenberg varieties, Adv. Math. 329 (2018), 955–1001. https://doi.org/10.1016/j.aim.2018.02.020
• A. Abreu and A. Nigro, Chromatic symmetric functions from the modular law, J. Combin. Theory Ser. A 180 (2021). https://doi.org/10.1016/j.jcta.2021.105407
• T. Hikita, A proof of the Stanley–Stembridge conjecture, arXiv:2410.12758 (2024, revised 2025). https://arxiv.org/abs/2410.12758v2
• S. T. Griffin, A. Mellit, M. Romero, K. Weigl and J. J. Wen, On Macdonald expansions of q-chromatic symmetric functions and the Stanley–Stembridge conjecture, arXiv:2504.06936 (2025). https://arxiv.org/abs/2504.06936v1
• OpenAI, Elementary positivity of chromatic quasisymmetric functions, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Corollary 1.2, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026/paper.pdf