∑math20

Combinatorics · Result 169

Shareshian–Wachs elementary positivity

1 paperLean

Resolves the elementary-positivity part of the Shareshian–Wachs conjecture: the chromatic quasisymmetric function of every natural unit interval graph has elementary-basis coefficients in \(\mathbb N[q]\). The coefficients count explicitly described permutations, giving a combinatorial explanation of positivity.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Elementary positivity of chromatic quasisymmetric functions

Elementary positivity of chromatic quasisymmetric functions

OpenAI · September 24, 2026

We prove that the chromatic quasisymmetric function of every natural unit interval graph is elementary-positive over \(\mathbb N[q]\). This resolves the elementary-positivity part of the Shareshian–Wachs conjecture.

Read PDF Download Source

Cite
@misc{OAI:Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026,
  author = {{OpenAI}},
  title = {{Elementary positivity of chromatic quasisymmetric functions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026/paper.pdf}{OAI:Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The elementary-positivity part of the Shareshian–Wachs conjecture asks whether the chromatic quasisymmetric function of every natural unit interval graph has nonnegative coefficients in the elementary basis. The formalization proves this over \(\mathbb N[q]\). It constructs an explicit elementary-basis expansion indexed by the graph's permitted nondescent permutations, with each term weighted by a nonnegative power of \(q\) determined by its graph inversions. The expansion holds for every finite number of color variables.

Comparator links

ResultComparator statement
Elementary positivity for natural unit interval graphsElementaryPositivity.lean

Scope note on GitHub →