AI Proved What?

Episode 169, October 2026

No minus signs?

A preprint claims that the colouring function of every natural unit interval graph has elementary coefficients that are polynomials in q with nonnegative coefficients, one permutation per term

Covers result 169 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

5:45. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:44The claim
  3. 3:17How the proof goes
  4. 4:54Where it stands

The claim, in plain words

Colour the vertices of a graph so that neighbours get different colours. Stanley’s chromatic symmetric function adds up, over all proper colourings, a product of variables x, one per vertex, chosen by its colour; Shareshian and Wachs weight each colouring by q to the number of edges whose lower-numbered end gets the smaller colour. Their graphs are natural unit interval graphs: unit intervals on a line, numbered from left to right, joined when they overlap. “The coloring definition already has nonnegative coefficients in the monomial variables, whereas rewriting it in the elementary basis can involve subtraction.” For the path 1–2–3 the answer is (1 + q + q2) e3 + q e21. As the paper recounts, the Stanley–Stembridge conjecture (1993) asks for elementary positivity at q = 1 for incomparability graphs of (3+1)-free posets; Guay-Paquet reduced it to unit interval orders; and Hikita proved it (first posted in 2024), with a formula that “gives numerical nonnegativity for every positive real q, while its rational q-weights do not establish coefficientwise nonnegativity in ℕ[q]”. Shareshian and Wachs had conjectured that every elementary coefficient lies in ℕ[q].

Result 169 is a single OpenAI preprint, Elementary positivity of chromatic quasisymmetric functions (51 pages, dated September 24, 2026). Theorem 1.1: “There is a deterministic terminating procedure which, given a natural unit interval graph G on [n] and σ ∈ DG0, returns a partition θG(σ) ⊢ n such that χG(X;q) = Σσ∈DG0 qginvG(σ) eθG(σ)(X). In particular every elementary coefficient of χG(X;q) belongs to ℕ[q].” Here DG0 is the set of permutations in which every drop between consecutive entries is an edge, and ginvG counts out-of-order pairs that are edges. “This proves the elementary-positivity part of the Shareshian–Wachs conjecture.” For the path, the permutations 123, 132, 213 and 321 have degrees 0, 1, 1 and 2; one of 132 and 213 goes to e21, and the other three to e3. At q = 1, with Guay-Paquet’s reduction, this recovers the Stanley–Stembridge theorem.

What it doesn’t claim

“The theorem makes no assertion of elementary unimodality”, the other half of the Shareshian–Wachs conjecture. Schur positivity was already known. The partition for each permutation comes from a long procedure: “The result proves termination, but gives no polynomial-time bound”, and “Equation (1.3) alone does not specify which of 132 and 213 receives which partition.” The positivity is proved algebraically (Corollary 5.9), and the permutation rule is built on top of it. With q, only natural unit interval graphs are covered. As our own illustration outside this class, Stanley’s function for the claw, one vertex joined to three others, is 4e4 + 5e31 − 2e22 + e211.

Where it stands

Posted as a preprint
OpenAI, 51 pages, dated September 24, 2026
Peer reviewed
Not yet
Checked in Lean
The identity and positivity, formalized by OpenAI; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statement asks for a partition label on DG0 making the paper’s identity hold, with coefficients in ℕ[q], for every number of colour variables. By our count the proof takes 549 files and 74,575 lines excluding Mathlib (the development), with no unproved steps by our search; we have not rebuilt it. The Lean exports its partition labels as the first table that passes a check against colouring counts; the paper-style construction is used only to prove that such a table exists, so the Lean does not compute the paper’s procedure. The Hessenberg corollary is not formalized, and the repository’s formalization list omits this result. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. A graph alphabet. One variable per vertex, where neighbours’ variables commute only up to a power of v, with q = v2. Sums over sets of vertices with no edges between them still commute, adapting a two-colour involution of Shareshian and Wachs, so they act like elementary functions of a phantom alphabet; each elementary coefficient becomes a coefficient of a monomial symmetric function there (Proposition 2.3), which normally needs subtraction: m21 = e2e1 − 3e3.
  2. Positive reordering. Reversing the order of a product of positive quantum factors gives such factors again with nonnegative whole-number multiplicities (Theorem 3.1), realized as dimensions of graded vector spaces built from shuffle algebras of Hall type.
  3. Walls and theta sections. In a scattering diagram, crossing a wall multiplies monomials by positive factors (Proposition 4.2), and theta-type sections stay positive in every chamber (Theorem 4.4).
  4. The triangular chart. The graph is placed in a chart with anchors and bridges; rotating the bridges, together with a support bound from powers of the first independent-set sum, forces each monomial function of the phantom alphabet to equal a theta section (Theorem 5.8). That gives positivity (Corollary 5.9).
  5. The witness. Each permutation is cut into packets, carried across walls by rank-matched bijections, and cleaned up by alternating paths in the Garsia–Milne tradition, until a weakly decreasing word of anchors remains; its letter counts are the partition (Theorem 6.7).

The numbers in the video

  • Our colourings: the path 1–2–3 with three colours has 12 proper colourings, with 0, 1 and 2 ascents 1, 10 and 1 times.
  • The path 1–2–3 (the paper’s example): (1 + q + q2) e3 + q e21. Ours, the path 1–2–3–4: (1 + q + q2 + q3) e4 + (q + q2) e31 + (q + q2) e22.
  • Our claw, outside the class, at q = 1: 4e4 + 5e31 − 2e22 + e211.
  • Our census: all 625 natural unit interval graphs with up to 7 vertices have elementary coefficients in ℕ[q], and their coefficients add up to the permutation count by graph inversions.
  • The Lean count: 549 files and 74,575 lines, our count of the import closure.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

Colour the vertices of a graph so that neighbours get different colours. Stanley turned all such colourings into one function: each colouring contributes a product of variables x, one for each vertex, chosen by its colour. Shareshian and Wachs added a second variable, q, counting the edges whose lower-numbered end gets the smaller colour. The graphs here are natural unit interval graphs: intervals of length one on a line, numbered from left to right, joined when they overlap. For the path 1–2–3, with three colours there are 12 proper colourings: one with no such ascent, ten with one, and one with two. Any symmetric function can be written in the elementary basis, built from e_k, the sum of all products of k different variables. Colourings give positive coefficients in plain monomials, but rewriting in this basis can involve subtraction. For the path, though, it comes out as (1 + q + q²) e_3 + q e_21: no minus signs. A 1993 conjecture of Stanley and Stembridge says, in this language, that with q = 1 this always happens for incomparability graphs of (3+1)-free posets, and Guay-Paquet reduced it to unit interval orders. Hikita proved the conjecture, first posted in 2024; as the paper notes, his formula gives nonnegative values at every positive q, but does not show it coefficient by coefficient. Shareshian and Wachs had conjectured that every coefficient is a polynomial in q with nonnegative whole-number coefficients. Outside this class it can fail: in our check, Stanley’s function for the claw, one vertex joined to three others, has a −2.

1:44The claim

Result 169 is a 51-page OpenAI preprint, dated September 24. Its theorem: for every natural unit interval graph, the function is a sum over certain permutations, those in which every drop between consecutive entries is an edge of the graph. Each is weighted by q to the number of its out-of-order pairs that are edges, times one elementary function, whose partition a deterministic, terminating procedure chooses for that permutation. So every coefficient lies in ℕ[q]. For the path, the four permutations 123, 132, 213 and 321 have degrees 0, 1, 1 and 2: one of the two degree-one permutations goes to e_21, and the other three go to e_3. At q = 1, with Guay-Paquet’s reduction, this recovers the Stanley–Stembridge theorem. Not claimed: that the coefficients are unimodal, the other half of the conjecture. Schur positivity was already known. Each permutation’s partition comes from a long procedure with no polynomial-time bound, and the paper does not say which degree-one permutation of the path gets e_21. The positivity itself is proved algebraically; the permutation rule is built on top of it. Only natural unit interval graphs are covered with q. In our check, all 625 such graphs with up to 7 vertices have coefficients in ℕ[q], and they add up to the permutation count.

3:17How the proof goes

The proof trades colourings for a graph alphabet: one variable per vertex, where the variables of neighbours do not commute, but pick up powers of q. Sums over sets of vertices with no edges between them still commute, by adapting a colour-swapping argument of Shareshian and Wachs, so they behave like elementary functions of a phantom alphabet. Each elementary coefficient becomes a coefficient of a monomial symmetric function in that alphabet, and those normally need subtraction: m_21 = e_2 e_1 − 3 e_3. The first key step is positive reordering: reversing the order of a product of positive quantum factors gives such factors again, with nonnegative whole-number multiplicities, which the paper realizes as dimensions of graded vector spaces, built from shuffle algebras of Hall type. Then come scattering diagrams: walls where crossing multiplies each monomial by positive factors, thanks to that reordering. Theta-type sections stay positive in every chamber. The graph-specific step places the graph in a triangular chart, with anchors and bridges, and shows that rotating the bridges, plus a support bound from powers of the first sum, forces each monomial function of the phantom alphabet to equal such a section; that gives positivity. Finally, the witness: each permutation is cut into packets, carried across walls by matched bijections, and cleaned up by alternating paths, until a weakly decreasing word of anchors remains, whose letter counts are the partition.

4:54Where it stands

The paper is a preprint, not peer reviewed, and not revised. Its identity, and so positivity in ℕ[q], is stated in Lean to match the paper, and OpenAI’s files contain a proof of about 75,000 lines, with no gaps we could find by search; we did not run the check. But the Lean picks each permutation’s partition by a search checked against colouring counts, not by the paper’s procedure. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, every natural unit interval graph has a colouring function whose elementary coefficients are polynomials in q with nonnegative coefficients, each term coming from a permutation. Unimodality is not claimed.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.