All missions

Motivation: does having a normal form imply termination?

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like $\ast$ and $\square$), axioms ($\ast:\square$) and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.

Timeline

• 1989 — Girard's Proofs and Types presents the Tait–Girard reducibility method for strong normalization (book).
• 1993 — Geuvers states the system-wide conjecture for β and βη reduction in his thesis (Logics and Type Systems, Nijmegen, Conjecture 8.1.2) (thesis).
• 1997 — Sørensen proves the implication for generalized nondependent, clean, negatable systems via continuation-passing translations (thesis, Copenhagen, Theorem 3.5.20).
• 2001 — Barthe, Hatcliff and Sørensen prove a uniform nondependent version (TCS 2001).
• 2006 — Barthe and Coquand show that erasing λ-domain annotations can identify non-convertible terms in non-normalizing PTSs (JFP 2006), a constraint on erasure-based approaches.
• 2014 — Roux and van Doorn develop a structural theory of PTSs, preserving weak normalization under sums and added rules (RTA–TLCA 2014).
• 2023 — Mull reduces the conjecture within tiered systems to an irrelevance-eliminating translation (TYPES 2022, LIPIcs 2023) and extends the nondependent results in his thesis (Chicago, 2023).
• 2025 — Roux proposes internal strong-normalization proofs for specific systems (TYPES 2025 abstract).
• 2026 — An OpenAI preprint, Weak and strong normalization in pure type systems (OpenAI Math Release, September 25, 2026), claims the β-version of the conjecture for every PTS, with no functionality assumption. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A specification consists of a type $S$ of sorts, an axiom relation $\mathcal A\subseteq S^2$ and a rule relation $\mathcal R\subseteq S^3$; neither is assumed functional. Expressions are

$$M,N,A,B ::= x\mid s\mid MN\mid \lambda x{:}A.\,M\mid \Pi x{:}A.\,B,\qquad s\in S,$$

up to renaming of bound variables. β-reduction is the compatible closure of $(\lambda x{:}A.M)N\to_\beta M[x:=N]$, with steps allowed everywhere, including inside the annotation $A$ of a λ and both parts of a Π. Typing $\Gamma\vdash M:A$ is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to $=_\beta$). A context is valid if each declared type is typed by a sort in the preceding prefix, and $M$ is legal in $\Gamma$ if $\Gamma\vdash M:A$ or $\Gamma\vdash A:M$ for some $A$.

The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.

Formalization targets

Goal: β-Barendregt–Geuvers–Klop (Theorem 1)

For every specification $\mathcal P=(S,\mathcal A,\mathcal R)$,

$$\bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is weakly }\beta\text{-normalizing}\bigr) \ \Longrightarrow\ \bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is strongly }\beta\text{-normalizing}\bigr).$$

Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.

Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.

Difficulty

The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.

Formalization scope

• Expressions use de Bruijn indices (Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.
• Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.
• HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.
• Weak normalization is reduction to a normal form; strong normalization is accessibility for the converse of Beta.
• The sort type S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.
• Needed infrastructure: renaming/substitution lemmas, confluence of β, subject reduction for PTSs, reducibility candidates. All are reusable for any PTS formalization.

Selected references

• J. H. Geuvers, Logics and Type Systems, PhD thesis, Katholieke Universiteit Nijmegen, 1993. https://www.cs.ru.nl/~herman/PUBS/Proefschrift.pdf
• J.-Y. Girard, Proofs and Types, Cambridge University Press, 1989. https://www.paultaylor.eu/stable/prot.pdf
• M. H. B. Sørensen, Normalization in λ-Calculus and Type Theory, PhD thesis, University of Copenhagen, 1997. https://di.ku.dk/forskning/Publikationer/tekniske_rapporter/tekniske-rapporter-1997/97-27.pdf
• G. Barthe, J. Hatcliff and M. H. Sørensen, Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoret. Comput. Sci. (2001). https://doi.org/10.1016/S0304-3975(01)00012-3
• G. Barthe and T. Coquand, Remarks on the equational theory of non-normalizing pure type systems, J. Funct. Programming (2006). https://doi.org/10.1017/S0956796803004726
• C. Roux and F. van Doorn, The structural theory of pure type systems, RTA–TLCA 2014. https://doi.org/10.1007/978-3-319-08918-8_25
• N. Mull, An irrelevancy-eliminating translation of pure type systems, TYPES 2022, LIPIcs, 2023. https://doi.org/10.4230/LIPIcs.TYPES.2022.7
• OpenAI, Weak and strong normalization in pure type systems, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf

Motivation

A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the $d$-regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer $\tanh\beta\le(d-1)^{-1/2}$ after proving it for large $d$ below a non-explicit constant (Nam–Sly–Zhang 2022).

This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1995–1996 — Bleher, Ruiz and Zagrebnov (J. Stat. Phys. 1995) and Ioffe (Lett. Math. Phys. 1996): the free state on the regular tree is extremal exactly when $(d-1)\tanh^2\beta\le1$.
• 2000 — Evans, Kenyon, Peres and Schulman relate broadcasting on trees to the Ising model (Ann. Appl. Probab. 2000).
• 2010 — Pemantle and Peres give a capacity criterion that also covers critical cases (Ann. Probab. 2010).
• 2015 — Backhausz, Szegedy and Virág's correlation bound for factors of IID (Random Struct. Alg. 2015), which rules out the free state beyond the threshold.
• 2017 — Lyons surveys factors of IID on trees, records Sly's obstruction above the reconstruction threshold, and the finite-cluster construction in the uniqueness range $\tanh\beta\le 1/(d-1)$ (CPC 2017).
• 2022 — Nam, Sly and Zhang construct the free state as a factor for $d\ge d_0$ and $\tanh\beta\le c/\sqrt{d-1}$, via posterior-drift stochastic differential equations, and conjecture the sharp threshold (CMP 2022).

Setting

Let $T_d$ be the infinite $d$-regular tree with vertex set $V$; concretely, $V$ is the set of finite words over $\{1,\dots,d\}$ with no two equal consecutive letters, and $w$ is adjacent to $wc$. Put $\theta=\tanh\beta$ for $\beta\ge0$. The free zero-field Ising law $\mu_{d,\beta}$ on $\{-1,+1\}^V$ is determined by its marginals on finite connected subtrees $D$:

$$\mu_{d,\beta}(\sigma|_D=\eta)=\frac12\prod_{\{u,v\}\in E(D)}\frac{1+\theta\,\eta_u\eta_v}{2}.$$

Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability $(1+\theta)/2$. A spin law is a factor of IID if it is the law of $\Phi(U)$ for i.i.d. uniform labels $U=(U_v)_{v\in V}$ and a measurable $\Phi:[0,1]^V\to\{-1,1\}^V$ such that, for each fixed automorphism $g$, $\Phi(gU)=g\Phi(U)$ almost surely, where $(gx)_v=x_{g^{-1}v}$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every integer $d\ge3$ and every $\beta\ge0$,

$$\mu_{d,\beta}\ \text{is a factor of IID}\iff \tanh\beta\le\frac1{\sqrt{d-1}}.$$

Significance

The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every $d\ge3$. The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ($\tanh\beta>(d-1)^{-1/2}$ excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.

Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.

Difficulty

Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range $\theta\le1/(d-1)$. The Nam–Sly–Zhang approach observes $X_v(t)=t\sigma_v+B_v(t)$ and expresses the posterior through innovations $W_v$, which are independent Brownian motions; but being Brownian does not make $X$ a function of $W$, and that is the central step (pp. 2–3). At criticality $\theta=(d-1)^{-1/2}$ the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).

Formalization scope

• TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.
• Labels have law Measure.infinitePi of Lebesgue measure on $[0,1]$; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.
• HasFreeIsingLaw θ μ prescribes $\mu$ on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.
• IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).
• The goal uses θ = Real.tanh β with $\beta\ge0$ and $d\ge3$; at $\beta=0$ both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.

Selected references

• OpenAI, The sharp factor-of-IID threshold for the free Ising model on regular trees, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026/article.pdf
• D. Nam, A. Sly, L. Zhang, Ising model on trees and factors of IID, Comm. Math. Phys. 389 (2022), 1009–1046. https://doi.org/10.1007/s00220-021-04260-2
• R. Lyons, Factors of IID on trees, Combin. Probab. Comput. 26 (2017), 285–300. https://doi.org/10.1017/S096354831600033X
• Á. Backhausz, B. Szegedy, B. Virág, Ramanujan graphings and correlation decay in local algorithms, Random Structures Algorithms 47 (2015). https://doi.org/10.1002/rsa.20562
• P. M. Bleher, J. Ruiz, V. A. Zagrebnov, On the purity of the limiting Gibbs state for the Ising model on the Bethe lattice, J. Stat. Phys. 79 (1995). https://doi.org/10.1007/BF02179399
• D. Ioffe, On the extremality of the disordered state for the Ising model on the Bethe lattice, Lett. Math. Phys. 37 (1996), 137–143. https://doi.org/10.1007/BF00416016
• W. Evans, C. Kenyon, Y. Peres, L. J. Schulman, Broadcasting on trees and the Ising model, Ann. Appl. Probab. 10 (2000). https://doi.org/10.1214/aoap/1019487349
• R. Pemantle, Y. Peres, The critical Ising model on trees, concave recursions and nonlinear capacity, Ann. Probab. 38 (2010). https://doi.org/10.1214/09-AOP482
• R. Eldan, Thin shell implies spectral gap up to polylog via a stochastic localization scheme, GAFA 23 (2013), 532–569. https://doi.org/10.1007/s00039-013-0214-y
• A. El Alaoui, A. Montanari, An information-theoretic view of stochastic localization, IEEE Trans. Inform. Theory 68 (2022). https://doi.org/10.1109/TIT.2022.3180298

Motivation

In Bernoulli bond percolation on a graph $G=(V,E)$, each edge is kept (open) independently with probability $p$. As $p$ grows, an infinite connected component of open edges appears at the critical probability $p_c(G)$. The criticality problem asks whether an infinite cluster can already exist at $p_c$. A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and $p_c<1$, there is no infinite cluster at $p_c$. The question contains the famous open case of $\mathbb Z^3$ and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.

Timeline

• 1957. Broadbent and Hammersley introduce percolation (doi:10.1017/S0305004100032680).
• 1960, 1980. Harris and Kesten settle nearest-neighbour bond percolation on $\mathbb Z^2$, including $\theta(p_c)=0$ (doi:10.1017/S0305004100034241, doi:10.1007/BF01197577).
• 1986–1987. Menshikov and Aizenman–Barsky prove sharpness of the subcritical phase; this does not settle behaviour at $p_c$ (doi:10.1007/BF01212322).
• 1990. Hara and Slade prove mean-field behaviour, including $\theta(p_c)=0$, for $\mathbb Z^d$ in sufficiently high dimension (doi:10.1007/BF02108785).
• 1996. Benjamini and Schramm formulate the conjecture for quasi-transitive graphs with $p_c<1$ (doi:10.1214/ECP.v1-978).
• 1999. Benjamini, Lyons, Peres and Schramm prove it for nonamenable graphs with a unimodular quasi-transitive action (doi:10.1214/aop/1022677450).
• 2006. Timár excludes infinitely many infinite critical clusters on nonunimodular transitive graphs (doi:10.1214/009117906000000494).
• 2016. Hutchcroft proves the conjecture for every quasi-transitive graph of exponential growth (arXiv:1605.05301). Duminil-Copin, Sidoravicius and Tassion treat slabs (doi:10.1002/cpa.21641).
• 2017. Fitzner and van der Hofstad reach nearest-neighbour $\mathbb Z^d$, $d\ge11$ (arXiv:1506.07977).
• 2021. Hermon and Hutchcroft cover certain groups of intermediate growth (arXiv:1809.11112).
• 2024. Kozma and Nitzan reduce the $\mathbb Z^d$ case to a conjectured gluing inequality (arXiv:2401.12397).
• 2026. Public, non-peer-reviewed announcements report AI-assisted proofs for $\mathbb Z^d$, including a reported Lean formalization of the lattice case (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.

Setting

A graph here has vertex set $V$ and a set $E$ of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on $V$. Examples include $\mathbb Z^d$ and every Cayley graph of a finitely generated group.

For $p\in[0,1]$, let $\mathbb P_p$ be the law of a random set $\omega\subseteq E$ containing each bond independently with probability $p$. The cluster $C_x(\omega)$ of $x$ is the set of vertices joined to $x$ by a finite path of bonds in $\omega$ (including $x$). Define

$$p_c(G)=\inf\{p\in[0,1]:\ \mathbb P_p(\exists x,\ |C_x|=\infty)>0\}.$$

Formalization targets

Goal: Theorem 1.1

For every infinite, connected, locally finite, quasi-transitive graph $G$,

$$p_c(G)<1\ \Longrightarrow\ \mathbb P_{p_c(G)}\bigl(\exists x\in V:\ |C_x|=\infty\bigr)=0.$$

The hypothesis $p_c<1$ is necessary, since at $p=1$ every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.

Significance

Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives $\theta(p_c)=0$ on $\mathbb Z^d$ for every $d\ge2$ (Corollary 10.1, p. 39), including the long-open case $d=3$. With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at $p_c$ on every such graph.

The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour $\mathbb Z^d$. A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.

Difficulty

The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.

Formalization scope

• BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.
• Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.
• law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.
• criticalProbability is sInf in unitInterval of $\{p:\mathbb P_p(\text{percolates})>0\}$; if the set were empty this would be $1$, which hpc excludes.
• percolates is the event that some cluster is infinite; the conclusion says it has measure $0$ at $p_c$.

A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.

Selected references

• OpenAI, No percolation at criticality on quasi-transitive graphs, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026/paper.pdf
• I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$, many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Critical percolation on any nonamenable group has no infinite clusters, Ann. Probab., 1999. https://doi.org/10.1214/aop/1022677450
• T. Hutchcroft, Critical percolation on any quasi-transitive graph of exponential growth has no infinite clusters, C. R. Math., 2016. https://doi.org/10.1016/j.crma.2016.07.013
• J. Hermon, T. Hutchcroft, No percolation at criticality on certain groups of intermediate growth, IMRN, 2021. https://doi.org/10.1093/imrn/rnz265
• R. Tessera, M. C. H. Tointon, A finitary structure theorem for vertex-transitive graphs of polynomial growth, Combinatorica, 2021. https://doi.org/10.1007/s00493-020-4295-6
• G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397
• T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
• H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
• Á. Timár, Percolation on nonunimodular transitive graphs, Ann. Probab., 2006. https://doi.org/10.1214/009117906000000494

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

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 Ramsey number $R(H,J)$ is the least $N$ such that every red–blue colouring of the edges of $K_N$ contains a red copy of $H$ or a blue copy of $J$. For a cycle $C_m$ against a clique $K_n$ there is a simple lower-bound construction: take $n-1$ disjoint red cliques of order $m-1$ with all edges between them blue. It has $(m-1)(n-1)$ vertices, no red $C_m$ (each red component is too small) and no blue $K_n$ (a blue clique meets each red clique at most once). In 1978 Erdős, Faudree, Rousseau and Schelp conjectured that this construction is optimal whenever $m\ge n\ge3$, apart from $R(C_3,K_3)=6$. Cycle–complete Ramsey numbers are among the few families where exact values are expected over a whole parameter range, and the conjecture has been attacked case by case for decades.

This mission asks for a formal proof of the full conjecture as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open. Part of the proof is a finite case analysis of 3,099 parameter-pattern instances carried out by two exact programs that accompany the paper.

Background

• 1971 — Chartrand and Schuster settle $n=3$ (Bull. AMS 1971).
• 1973 — Bondy and Erdős prove the formula for $m\ge n^2-2$ (JCTB 1973).
• 1978 — Erdős, Faudree, Rousseau and Schelp state the conjecture (J. Graph Theory 1978).
• 1999–2008 — The full range for $n=4$ (Yang–Huang–Zhang, Australas. J. Combin. 1999), $n=5$ (Bollobás et al., Australas. J. Combin. 2000), $n=6$ (Schiermeyer, JGT 2003), $n=7$ (Chen–Cheng–Zhang, Eur. J. Combin. 2008).
• 2005 — Nikiforov proves the formula for $n\ge4$, $m\ge4n+2$ (CPC 2005).
• 2007–2023 — Partial results for $n=8$, including $R(C_8,K_8)$ (Discrete Math. 2009) and $R(C_9,K_8)$ (ISRN Algebra 2011).
• 2021 — Keevash, Long and Skokan prove the formula for $m\ge C\log n/\log\log n$, leaving finitely many open pairs (IMRN 2021).
• September 2026 — The OpenAI preprint claims all remaining pairs (Theorem 1.1, p. 2).

Setting

All graphs are finite and simple. $C_m$ is the cycle on exactly $m$ vertices and $K_n$ the complete graph on $n$ vertices. Identify a red–blue colouring of $K_N$ with its red graph $G$ on $N$ vertices; the blue graph is the complement $\overline G$. A copy of $H$ in $G$ is an injective homomorphism $H\to G$ (copies need not be induced). The Ramsey property $\mathcal R(m,n,N)$ says: every graph $G$ on $N$ vertices contains $C_m$ or its complement contains $K_n$. Then

$$R(C_m,K_n)=\min\{N:\ \mathcal R(m,n,N)\}.$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

For all integers $m\ge n\ge 3$ with $(m,n)\ne(3,3)$,

$$R(C_m,K_n)=(m-1)(n-1)+1,$$

and $R(C_3,K_3)=6$.

Significance

The result itself. It completes a programme that over five decades settled the conjecture for $n\le7$, for long cycles, and for all sufficiently large $n$ by Keevash–Long–Skokan; the preprint's contribution is the remaining finite but large set of pairs. Since Keevash–Long–Skokan's constant is not explicit, the preprint gives a structural reduction that does not need a numerical value of it.

Formalizing it. The statement uses only Mathlib's cycleGraph, complete graphs, complements and subgraph containment. A formal proof would have to certify both the structural lemmas (independent-set expansion, a large-clique lemma, optimal path systems) and the finite verification of 3,099 pattern instances, which the preprint currently delegates to two programs with deduction traces. Bringing such a computation inside a proof assistant is itself a worthwhile contribution. Neither $R(C_m,K_n)$ for general parameters nor any of the previously known infinite families has a machine-checked proof.

Difficulty

The lower bound is the explicit construction above; the work is the upper bound for exact cycle length $m$. Methods that find long cycles (Pósa rotation, Chvátal–Erdős) produce cycles of length at least $m$, not exactly $m$, and forbidding exactly one cycle length gives weak structural information. The preprint passes to a minimal counterexample with independent-set expansion (Lemma 2.2, p. 4), finds a clique of order $\max\{3,\lfloor k/2\rfloor\}$ with $k=m-1$ (Theorem 3.1, p. 5), and optimizes systems of paths through that clique so that every improvement would close a cycle of order exactly $m$. Cliques of order $t\ge9$ are excluded by hand (Proposition 8.4, p. 24); the remaining $3\le t\le8$, $5\le k\le17$ need the finite verification of Section 9 (Proposition 9.1, p. 26).

Formalization scope

• RamseyProperty m n N: for every G : SimpleGraph (Fin N), cycleGraph m ⊑ G or (⊤ : SimpleGraph (Fin n)) ⊑ Gᶜ, where ⊑ is Mathlib's subgraph containment (injective homomorphism, non-induced).
• cycleCliqueRamsey m n = sInf {N | RamseyProperty m n N} in ℕ. If the set were empty, sInf would return 0; the goal's equalities exclude that, so a proof must exhibit the Ramsey property.
• The goal quantifies over integers $m,n$ with $3\le n\le m$, $(m,n)\ne(3,3)$, converting with toNat (harmless since both are at least $3$), and separately states cycleCliqueRamsey 3 3 = 6.
• cycleGraph m on Fin m is the $m$-cycle for $m\ge3$.

Welcome contributions: a verified checker for the pattern enumeration of Section 9, and the classical small cases ($n=3$, Bondy–Erdős for $m\ge n^2-2$).

Selected references

• OpenAI, Cycle–clique Ramsey numbers, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Cycle-clique-Ramsey-numbers-September-25-2026/Cycle-clique-Ramsey-numbers-September-25-2026.pdf
• P. Erdős, R. J. Faudree, C. C. Rousseau, R. H. Schelp, On cycle–complete graph Ramsey numbers, J. Graph Theory 2 (1978). https://doi.org/10.1002/jgt.3190020107
• J. A. Bondy, P. Erdős, Ramsey numbers for cycles in graphs, J. Combin. Theory Ser. B (1973). https://doi.org/10.1016/S0095-8956(73)80005-X
• G. Chartrand, S. Schuster, On the existence of specified cycles in complementary graphs, Bull. Amer. Math. Soc. (1971). https://doi.org/10.1090/S0002-9904-1971-12832-X
• I. Schiermeyer, All cycle-complete graph Ramsey numbers r(C_m,K_6), J. Graph Theory (2003). https://doi.org/10.1002/jgt.10145
• V. Nikiforov, The cycle-complete graph Ramsey numbers, Combin. Probab. Comput. (2005). https://doi.org/10.1017/S096354830400642X
• Y. Chen, T. C. E. Cheng, Y. Zhang, The Ramsey numbers R(C_m,K_7) and R(C_7,K_8), European J. Combin. (2008). https://doi.org/10.1016/j.ejc.2007.05.007
• P. Keevash, E. Long, J. Skokan, Cycle-complete Ramsey numbers, Int. Math. Res. Not. (2021). https://doi.org/10.1093/imrn/rnz119
• V. Chvátal, P. Erdős, A note on Hamiltonian circuits, Discrete Math. (1972). https://doi.org/10.1016/0012-365X(72)90079-9

Motivation

A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness $C/k$ in every $k$-edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.

Background. The maximum-entropy rounding of Asadpour et al. constructs $O(\log n/(k\log\log n))$-thin trees. Oveis Gharan and Saberi constructed $O(1/k)$-thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of $\mathrm{poly}(\log\log n)/k$-thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.

Setting

Graphs are finite undirected loopless multigraphs; parallel copies count separately. For $\varnothing\ne S\subsetneq V(G)$, $\delta_G(S)$ is the multiset of edges with exactly one endpoint in $S$, and $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for all such $S$. Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.

Formalization targets

Goal: Theorem 1.1 (algorithmic strong thin trees)

There is an absolute constant $C$ and a deterministic algorithm that, given $k\ge1$ and a $k$-edge-connected multigraph $G$ on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree $T$ with

$$|\delta_T(S)|\le\frac Ck\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G)),$$

returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.

Significance

The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do $C/k$-thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order $1/k$ is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.

Formalization scope

• Graphs: StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).
• Valid x: $n\ge1$, $k\ge1$ and EdgeConnected k.
• The machine model is CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).
• AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for $n=1$ the output is empty.
• One machine and one polynomial serve all inputs in both formats.

Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.

Selected references

• OpenAI, A polynomial-time construction of strong thin trees, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026/paper.pdf
• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026.
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
• N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
• S. Oveis Gharan, A. Saberi, The asymmetric traveling salesman problem on graphs with bounded genus, SODA, 2011. https://doi.org/10.1137/1.9781611973082.75
• N. Klein, N. Olver, Thin trees for laminar families, FOCS, 2023. https://doi.org/10.1109/FOCS57990.2023.00011
• N. Klein, N. Olver, Z. S. Yeoh, Thin trees for near minimum cuts, ICALP, 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.129
• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM, 2020. https://doi.org/10.1145/3424306

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

Motivation

Kazhdan–Lusztig polynomials $P_{u,b}(q)$ are integer polynomials attached to pairs $u\le b$ of elements of a Coxeter group. They were introduced through the canonical basis of the Hecke algebra (Kazhdan–Lusztig, 1979). For Weyl groups they compute local intersection cohomology of Schubert varieties, and they enter the Kazhdan–Lusztig conjectures on characters of highest-weight representations. Their definition uses the simple generators of the group, yet in every known example $P_{u,b}$ seemed to depend only on the Bruhat interval $[u,b]$ as an abstract partially ordered set. The combinatorial invariance conjecture, attributed to Lusztig and Dyer, asserts this: if two Bruhat intervals, possibly in different Coxeter groups, are isomorphic as posets, their Kazhdan–Lusztig polynomials coincide.

This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1979–1980 — Kazhdan and Lusztig define the polynomials (Invent. Math. 1979) and interpret them via Schubert varieties (Proc. Sympos. Pure Math. 36, 1980).
• 1987–1993 — Dyer's thesis and papers on reflection subgroups and the Bruhat graph (J. Algebra 1990; Compositio 1991); the conjecture's published formulation for finite Coxeter systems and the reconstruction of the Bruhat graph from the interval order.
• 2000–2006 — Lower intervals $[1,b]$: du Cloux (Adv. Math. 2003), Brenti for symmetric groups (EJC 2004), and for all Coxeter systems Brenti–Caselli–Marietti (Adv. Math. 2006) and Delanoy (J. Alg. Combin. 2006).
• 2001–2014 — Moment-graph and Soergel-bimodule machinery: Braden–MacPherson (Math. Ann. 2001), Fiebig (Trans. AMS 2008), Soergel (J. Inst. Math. Jussieu 2007), Elias–Williamson (Annals 2014).
• 2007–2021 — Short intervals (Incitti, JCTA 2007); the coefficient of $q$ in simply-laced type (Patimo, IMRN 2021).
• 2022–2026 — Hypercube decompositions guided by machine learning (Blundell–Buesing–Davies–Veličković–Williamson, Represent. Theory 2022); Barkley–Gaetz (Math. Ann. 2025; IMRN 2026); Barkley–Gaetz–Lam: invariance of the $q$-coefficient in general and full invariance up to rank six (arXiv:2601.07793); Esposito–Marietti–Stella up to rank ten in finite Weyl groups (arXiv:2509.16433).
• September 2026 — The OpenAI preprint claims the full conjecture for arbitrary Coxeter systems (Theorem 1.1, p. 2).

Setting

A Coxeter system $(W,S)$ is a group $W$ with a generating set $S$ of involutions subject only to relations $(st)^{m_{st}}=1$. Write $\ell$ for word length in $S$. A reflection is a conjugate of an element of $S$. Bruhat order is the partial order generated by $x<tx$ whenever $t$ is a reflection and $\ell(tx)>\ell(x)$; the interval $[u,b]=\{x:u\le x\le b\}$ is finite and graded of rank $\ell(b)-\ell(u)$, even when $W$ is infinite. The equal-parameter R-polynomials $R_{x,y}$ and Kazhdan–Lusztig polynomials $P_{x,y}$ are the unique families with $R_{x,x}=P_{x,x}=1$, $R_{x,y}=P_{x,y}=0$ unless $x\le y$, the recursion: for $s\in S$ with $sy<y$,

$$R_{x,y}=\begin{cases}R_{sx,sy}, & sx<x,\\ (q-1)R_{x,sy}+q\,R_{sx,sy}, & sx>x,\end{cases}$$

the degree bound $\deg P_{x,y}<(\ell(y)-\ell(x))/2$ for $x<y$, and the inversion formula

$$q^{\ell(y)-\ell(x)}P_{x,y}(q^{-1})=\sum_{x\le z\le y}R_{x,z}(q)\,P_{z,y}(q).$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

Let $(W,S)$ and $(W',S')$ be arbitrary Coxeter systems, $u\le b$ in $W$ and $u'\le b'$ in $W'$. If $\iota:[u,b]\to[u',b']$ is an isomorphism of posets (a bijection preserving and reflecting order), then

$$P^{W}_{u,b}(q)=P^{W'}_{u',b'}(q).$$

The isomorphism carries no labels or root data; the groups may be infinite and noncrystallographic.

Significance

The result itself. It shows that a Kazhdan–Lusztig polynomial, defined algebraically from the Hecke algebra, is determined by a finite poset. Restricting $\iota$ to subintervals gives the same for every $P_{x,y}$ with $u\le x\le y\le b$, and hence for the R-polynomials (Corollary 6.1, p. 29). For Weyl groups this means that local intersection cohomology of Schubert varieties is determined by the Bruhat poset. It settles a question open since the 1980s that had been verified only for lower intervals, short intervals, low ranks, and single coefficients.

Formalizing it. Mathlib has Coxeter systems and their length function but no Bruhat order, Hecke algebra, or Kazhdan–Lusztig theory. The proof uses reflection orders (Dyer's path formula, Theorem 2.2, p. 7), Braden–MacPherson moment-graph sheaves over a reflection-faithful real realization (Theorem 2.3, p. 8), and the Elias–Williamson character theorem as external inputs. Building these would be a substantial, reusable contribution to formal representation theory.

Difficulty

The defining recursion uses a simple generator $s$ with $sy<y$, but a poset isomorphism need not carry simple generators or reflections to anything recognisable, and need not respect root labels. Dyer's reconstruction recovers all reflection edges of the Bruhat graph from the order (Theorem 3.4, p. 12) but not their labels. Lanini's moment-graph invariance requires compatible label automorphisms, which an abstract isomorphism does not provide. The preprint therefore keeps the two realizations separate, transports reflection orders through maximal dihedral subintervals (Proposition 3.5, p. 13), counts later edges exactly, and compares images of edges in two different sheaves by a reciprocal inequality that is then forced to be an equality (Sections 5–6).

Formalization scope

• Coxeter systems are Mathlib CoxeterSystem M W for arbitrary index types and groups; the two systems may live in different universes.
• BruhatLE is the reflexive–transitive closure of $x\to tx$ with $t$ a reflection and $\ell(x)<\ell(tx)$, i.e. strong Bruhat order (not weak order). Interval cs u b carries this order; ι is an order isomorphism ≃o.
• klPolynomial is the second component of Classical.epsilon (NormalizedKL cs), where NormalizedKL encodes exactly the normalization above (R-recursion with left multiplication, diagonal and vanishing conditions, $2\deg P<\ell(y)-\ell(x)$, and the inversion formula with Polynomial.reflect). Existence and uniqueness of such families is the classical Kazhdan–Lusztig theorem, and a proof of the goal has to establish them, since otherwise Classical.epsilon returns an arbitrary pair.
• Sums over intervals use finsum; intervals are finite, so this is the ordinary sum.
• The hypotheses $u\le b$, $u'\le b'$ are explicit; there is no vacuous reading.

Welcome contributions: Bruhat order and its basic properties (subword property, finiteness of intervals), R-polynomials, and existence and uniqueness of Kazhdan–Lusztig polynomials for arbitrary Coxeter systems.

Selected references

• OpenAI, Combinatorial invariance of Kazhdan–Lusztig polynomials, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Combinatorial-Invariance-of-Kazhdan-Lusztig-Polynomials-September-24-2026/paper.pdf
• D. Kazhdan, G. Lusztig, Representations of Coxeter groups and Hecke algebras, Invent. Math. 53 (1979), 165–184. https://doi.org/10.1007/BF01390031
• M. Dyer, On the "Bruhat graph" of a Coxeter system, Compositio Math. 78 (1991), 185–191. https://www.numdam.org/item/CM_1991__78_2_185_0/
• F. Brenti, F. Caselli, M. Marietti, Special matchings and Kazhdan–Lusztig polynomials, Adv. Math. 202 (2006), 555–601. https://doi.org/10.1016/j.aim.2005.01.011
• E. Delanoy, Combinatorial invariance of Kazhdan–Lusztig polynomials on intervals starting from the identity, J. Algebraic Combin. 24 (2006), 437–463. https://doi.org/10.1007/s10801-006-0014-7
• F. du Cloux, Rigidity of Schubert closures and invariance of Kazhdan–Lusztig polynomials, Adv. Math. 180 (2003), 146–175. https://doi.org/10.1016/S0001-8708(02)00100-7
• T. Braden, R. MacPherson, From moment graphs to intersection cohomology, Math. Ann. 321 (2001), 533–551. https://doi.org/10.1007/s002080100232
• B. Elias, G. Williamson, The Hodge theory of Soergel bimodules, Ann. of Math. 180 (2014), 1089–1136. https://doi.org/10.4007/annals.2014.180.3.6
• C. Blundell, L. Buesing, A. Davies, P. Veličković, G. Williamson, Towards combinatorial invariance for Kazhdan–Lusztig polynomials, Represent. Theory 26 (2022), 1145–1191. https://doi.org/10.1090/ert/624
• G. T. Barkley, C. Gaetz, T. Lam, Combinatorial invariance for the coefficient of q in Kazhdan–Lusztig polynomials, arXiv:2601.07793 (2026). https://arxiv.org/abs/2601.07793v2
• A. Björner, F. Brenti, Combinatorics of Coxeter Groups, GTM 231, Springer, 2005. https://doi.org/10.1007/3-540-27596-7

Motivation

A vertex cover of a hypergraph $H$ is a set of vertices meeting every edge; the covering number $\tau(H)$ is the minimum size of a cover, and the matching number $\nu(H)$ is the maximum number of pairwise disjoint edges. In an $r$-partite $r$-uniform hypergraph the vertices are split into $r$ parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts

$$\tau(H)\le(r-1)\,\nu(H).$$

For $r=2$ it is Kőnig's theorem, so it proposes a higher-dimensional analogue of the most basic min–max theorem of bipartite matching theory. In the intersecting case ($\nu=1$) it asks for a cover of size $r-1$, and it is equivalent to Gyárfás's conjecture that $r-1$ monochromatic trees cover any $r$-edge-coloured complete graph.

Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case $r=3$ in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through $r=5$; Haxell and Scott (2012) proved $\tau\le(r-\epsilon)\nu$ for $r=4,5$ (doi:10.37236/1175); Francetić, Herke, McKay and Wanless (2017) handled linear intersecting hypergraphs through rank nine (doi:10.1016/j.ejc.2016.10.004); Bishnoi, Das, Morris and Szabó (2021) treated $t$-intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever $r-1$ is a prime power; equality examples were studied by Mansour, Song and Yuster (2009, doi:10.1007/s00373-008-0821-9), Aharoni, Barát and Wanless (2016, doi:10.1007/s00373-015-1575-9) and Abu-Khazneh, Barát, Pokrovskiy and Szabó (2019, doi:10.1016/j.jcta.2018.07.011). Clow, Haxell and Mohar disproved Lovász's stronger matching-reduction conjecture at $r=3$ (doi:10.1007/s00493-026-00220-3), without contradicting Ryser's inequality.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims intersecting counterexamples for ranks $r=s^n+1$.

Setting

A finite hypergraph is a finite set of edges, each a finite set of vertices. It is $r$-partite $r$-uniform if there is a map assigning each vertex one of $r$ parts such that every edge contains exactly one vertex of each part. It is intersecting if it is nonempty and any two distinct edges share a vertex, so $\nu(H)=1$. Every edge of an intersecting hypergraph is itself a cover, so $\tau(H)\le r$ always; a counterexample to Ryser's conjecture in the intersecting case needs $\tau(H)=r$.

Formalization targets

Milestone: special case of Theorem 1.1

There are a prime $p>5$ with $p\equiv2\pmod3$ and $N$ such that for every prime $n\ge N$, $n>2$, an intersecting $(p^n+1)$-partite $(p^n+1)$-uniform hypergraph with $\nu=1$ and $\tau=p^n+1$ exists.

Goal: Theorem 1.1

There is $s_0$ such that for every prime $s\ge s_0$ with $s\equiv2\pmod 3$ there is $n_0(s)\ge3$ such that for every odd $n\ge n_0(s)$, with $q=s^n$, there is a finite intersecting $(q+1)$-partite $(q+1)$-uniform hypergraph $H$ with

$$\tau(H)=q+1>q=(r-1)\,\nu(H).$$

In particular infinitely many ranks fail. Lean: OAI.RyserOdd.eventualOddFailures_and_infinite, open on the platform.

Significance

The theorem would disprove Ryser's conjecture in its intersecting case, and through the standard transfer (Corollary 1.2) also Gyárfás's monochromatic tree-cover conjecture, for the ranks $s^n+1$. The value $\tau=r$ is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime $q$, with balanced parts); the two constructions are independent apart from three elementary estimates. Thresholds are not numerical. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

The truncated-plane examples sit exactly at $\tau=r-1$, and covers may mix vertices from different parts, so enlarging individual parts does not help. One must insert exceptional edges that destroy every cover of size $q$ while preserving the intersecting property. Ruling out all small covers requires showing that any small cover contains almost a full pencil of lines, which over $\mathbb F_{s^n}$ needs an incidence bound with a power saving (a Bourgain–Katz–Tao-type sum–product estimate) valid in fields whose proper subfields are small. This is where odd exponents and the congruence $s\equiv2\pmod3$ enter.

Formalization scope

• Hypergraph V := Finset (Finset V) over a finite type V with decidable equality.
• RPartiteUniform r H: some part : V → Fin r with exactly one vertex of each part in every edge. Uniform r H: every edge has r vertices.
• Intersecting: distinct edges meet. matchingNumber is the maximal size of a pairwise disjoint subfamily; coverNumber is sInf of cover sizes, and existence of a cover is asserted separately so the sInf is not the empty-set default.
• ExplicitFailureAt r packages all of these with $\nu=1$, $\tau=r$ and $(r-1)\nu<\tau$; the goal asserts it for the stated ranks and that the set of failing ranks is infinite.

Needed infrastructure: finite fields $\mathbb F_{s^n}$ and their projective planes, incidence and sum–product estimates, and probabilistic selection arguments. Contributions formalizing Theorem 2.1 (uniform incidence saving), Lemma 3.2 (line covers after random deletions) or Theorem 4.1 (compatible translates from independent pools) are welcome.

Selected references

• OpenAI, A counterexample to Ryser's covering conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf
• J. R. Henderson, Permutation decompositions of (0,1)-matrices and decomposition transversals, PhD thesis, 1971. https://doi.org/10.7907/J1Z1-SK19
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica, 2001. https://doi.org/10.1007/s004930170001
• P. Haxell, A. Scott, On Ryser's conjecture, Electron. J. Combin., 2012. https://doi.org/10.37236/1175
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin., 2017. https://doi.org/10.1016/j.ejc.2016.10.004
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A, 2019. https://doi.org/10.1016/j.jcta.2018.07.011
• J. Bourgain, N. Katz, T. Tao, A sum-product estimate in finite fields, and applications, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0451-1
• A. Clow, P. Haxell, B. Mohar, A counterexample to a conjecture of Lovász, Combinatorica, 2026. https://doi.org/10.1007/s00493-026-00220-3
• OpenAI, Balanced counterexamples to Ryser's conjecture at prime orders, preprint, September 27, 2026.

Motivation

In metric $k$-median, a finite set $J$ (or $D$) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$, one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

$$\mathrm{cost}(S)=\sum_{j\in J}d(j,S),\qquad d(j,S)=\min_{i\in S}d(j,i),\qquad \mathrm{OPT}_k=\min_{S\subseteq F,\ 1\le|S|\le k}\mathrm{cost}(S).$$

Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if $\mathrm P\ne\mathrm{NP}$, no polynomial-time algorithm achieves a factor below $1+2/e\approx1.736$ in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached $2+\varepsilon$, leaving a gap between $1.736$ and $2$.

This mission asks for a formal proof that the threshold is exactly $1+2/e$, as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time $(1+2/e+\varepsilon)$-approximation for every fixed $\varepsilon>0$, and hence, under $\mathrm P\ne\mathrm{NP}$, an infimal approximation factor of exactly $1+2/e$. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 2001–2002 — Jain and Vazirani connect $k$-median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
• 2004 — Arya et al. show that bounded-swap local search achieves $3+\varepsilon$ (SICOMP 2004).
• 2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor-$3$ barrier (SICOMP 2016).
• 2017–2023 — Bi-point rounding: $2.675+\varepsilon$ (Byrka et al., TALG 2017) and $2.613$ (Gowda et al., SODA 2023).
• 2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT $(1+2/e+\varepsilon)$-approximation in time $k^{O(k)}\mathrm{poly}$ (ICALP 2019).
• 2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach $2+\varepsilon$ (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with $2+\varepsilon$ (arXiv:2604.06046).
• September 2026 — Two OpenAI preprints claim a deterministic $(1+2/e+\varepsilon)$-approximation, matching the known hardness threshold (source), and an independent randomized $(2-\sigma)$-approximation via anchor recovery and bounded-price strictness (source).
• Hardness — Feige proves the $\ln n$ threshold for set cover and the perfect-completeness Max-$k$-Coverage gap (J. ACM 1998, Theorem 5.3); Anand and Lee record the resulting $1+2/e$ lower bound for $k$-median with specified facilities under $\mathrm P\ne\mathrm{NP}$ (IPCO 2024).

Setting

An instance consists of $n$ points with a rational distance table $d$ that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set $J$, a facility set $F$ (index sets that may overlap), and an integer $1\le k\le|F|$, encoded in binary. A feasible solution is a nonempty $S\subseteq F$ with $|S|\le k$. An algorithm is an $\alpha$-approximation if it always outputs a feasible $S$ with $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$, and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.

Formalization targets

Milestone: Theorem 1.1 (p. 1)

For every fixed $\varepsilon>0$ there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible $S$ with

$$\sum_{j\in J}d(j,S)\le\Bigl(1+\frac2e+\varepsilon\Bigr)\mathrm{OPT}_k .$$

Goal: Corollary 1.2 (p. 2)

If $\mathrm P\ne\mathrm{NP}$, then

$$\inf\{\alpha:\ \text{a deterministic polynomial-time }\alpha\text{-approximation exists}\}=1+\frac2e .$$

The infimum is not asserted to be attained.

Significance

The result itself. It closes the approximability of metric $k$-median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search ($3+\varepsilon$), bi-point rounding ($2.675$, $2.613$) to $2+\varepsilon$. It shows that the FPT factor $1+2/e$ of Cohen-Addad et al. is achievable in polynomial time. The case $F=J$ has a different and still separate lower-bound question.

Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.

Difficulty

Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least $2$ (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max-$k$-Coverage gap.

Formalization scope

• Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size $\le k$.
• Outputs are membership bit masks of an actual feasible set; FactorCorrect α I out requires that mask to describe a nonempty $S\subseteq F$ with $|S|\le k$ and $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$.
• Polynomial time is Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.
• approximationFactors is the set of $\alpha$ admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.
• The hypothesis $\mathrm P\ne\mathrm{NP}$ is not provable, so the goal is a conditional statement; deriving the lower bound requires a Cook–Levin-type NP-hardness of the coverage gap in this model.

Selected references

• OpenAI, The approximation threshold for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf
• OpenAI, Single-exponential recovery and bounded-price strictness for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf
• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45 (1998). https://doi.org/10.1145/285055.285059
• A. Anand, E. Lee, Separating k-median from the supplier version, IPCO 2024. https://doi.org/10.1007/978-3-031-59835-7_2
• K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
• M. Charikar, S. Li, A dependent LP-rounding approach for the k-median problem, ICALP 2012. https://doi.org/10.1007/978-3-642-31594-7_17
• R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, J. ACM 53 (2006). https://doi.org/10.1145/1147954.1147956
• K. N. Gowda, T. Pensyl, A. Srinivasan, K. Trinh, Improved bi-point rounding algorithms and a golden barrier for k-median, SODA 2023. https://doi.org/10.1137/1.9781611977554.ch38
• K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
• M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
• S. Li, O. Svensson, Approximating k-median via pseudo-approximation, SIAM J. Comput. 45 (2016). https://doi.org/10.1137/130938645
• J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
• V. Cohen-Addad, A. Gupta, A. Kumar, E. Lee, J. Li, Tight FPT approximations for k-median and k-means, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.42
• V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2