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