Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Elementary positivity for natural unit interval graphs

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Definition selected for comparison: OAI.elementaryPositivityWitness

Lean statement file: ElementaryPositivity.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 169 link it.

See the candidate theoremWho ran the proof-verification programReport a comparison with the paper (GitHub issue)

Problems reported

  • Correction The configuration had no theorem target, only a definition hole; the fork states the claim as a theorem that a witness exists (elementaryPositivityWitness_nonempty) and the release's construction proves it. Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 2026-10-11 Source

The Lean statement

The verification settings name no theorem. Comparator instead tests whether OpenAI’s library defines elementaryPositivityWitness with the types written here. The list below follows names used by those definitions; each appears after the names it uses.

def elementaryPositivityWitness (n : ℕ)    (G : ElementaryPositivity.NaturalUnitIntervalGraph n) :    G.PermutationWitness := by  sorry

For a definition marked “name and type only”, Comparator does not compare the definition’s body with the one here. When a theorem is configured, it verifies the proof using the definition in OpenAI’s library. Follow the library link to compare the two definitions.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • structure OAI.ElementaryPositivity.NaturalUnitIntervalGraph line 7

    structure NaturalUnitIntervalGraph (n : ℕ) where  h : Fin n → Fin n  increasing : Monotone h  extensive : ∀ i, i ≤ h i

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.Edge line 16

    def Edge (i j : Fin n) : Prop :=  (i < j ∧ j ≤ G.h i) ∨ (j < i ∧ i ≤ G.h j)

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.Nondescent line 22

    def Nondescent (σ : Equiv.Perm (Fin n)) : Prop :=  ∀ i j : Fin n, i.val + 1 = j.val → σ j < σ i → G.Edge (σ i) (σ j)

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.graphInversions line 29

    def graphInversions (σ : Equiv.Perm (Fin n)) : ℕ :=  (Finset.univ.filter fun ij : Fin n × Fin n =>    ij.1 < ij.2 ∧ σ ij.2 < σ ij.1 ∧ G.Edge (σ ij.1) (σ ij.2)).card

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.Proper line 33

    def Proper {r : ℕ} (f : Fin n → Fin r) : Prop :=  ∀ i j : Fin n, G.Edge i j → f i ≠ f j

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.coloringAscents line 39

    def coloringAscents {r : ℕ} (f : Fin n → Fin r) : ℕ :=  (Finset.univ.filter fun ij : Fin n × Fin n =>    ij.1 < ij.2 ∧ G.Edge ij.1 ij.2 ∧ f ij.1 < f ij.2).card

  • definition OAI.ElementaryPositivity.NaturalUnitIntervalGraph.chromatic line 43

    noncomputable def chromatic (r : ℕ) : MvPolynomial (Fin r) (Polynomial ℕ) :=  ∑ f ∈ Finset.univ.filter (G.Proper (r := r)),    MvPolynomial.C (Polynomial.X ^ G.coloringAscents f) *      ∏ i : Fin n, MvPolynomial.X (f i)

  • structure OAI.ElementaryPositivity.NaturalUnitIntervalGraph.PermutationWitness line 48

    structure PermutationWitness where  theta : {σ : Equiv.Perm (Fin n) // G.Nondescent σ} → Nat.Partition n  expansion : ∀ r : ℕ, G.chromatic r =    ∑ σ : {σ : Equiv.Perm (Fin n) // G.Nondescent σ},      MvPolynomial.C (Polynomial.X ^ G.graphInversions σ.val) *        MvPolynomial.esymmPart (Fin r) (Polynomial ℕ) (theta σ)

Definitions taken from OpenAI’s library 1

Comparator compares only the name and type of each definition listed here. When a theorem is configured, its proof uses the definition in OpenAI’s solution library. Read that definition as well as the one in this file when comparing the statement with the paper.

  • Comparator checks the name and type of elementaryPositivityWitness; its definition is in OpenAI’s library, in the modules that OAI.Combinatorics.Chromatic.Main imports.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: positivity, witness, permutation, natural, partition, interval, elementary, graph and two more. Found in the paper’s title, which its main theorem states: chromatic.

Theorem 1.1 of Elementary positivity of chromatic quasisymmetric functions

Theorem (Elementary positivity and a permutation witness)

There is a deterministic terminating procedure which, given a natural unit interval graph G on [n] and \sigma\in D_G^0, returns a partition \theta_G(\sigma)\vdash n such that

\chi_G(X;q)=\sum_{\sigma\in D_G^0} q^{\ginv_G(\sigma)}e_{\theta_G(\sigma)}(X).

In particular every elementary coefficient of \chi_G(X;q) belongs to \N[q]. The assertion holds as a formal symmetric-function identity, uniformly in n and G.

Section 1, Introduction Read it in the paper TeX source, line 39
Show the TeX
There is a deterministic terminating procedure which, given a natural
unit interval graph $G$ on $[n]$ and $\sigma\in D_G^0$, returns a partition
$\theta_G(\sigma)\vdash n$ such that
\begin{equation}
 \chi_G(X;q)=\sum_{\sigma\in D_G^0}
       q^{\ginv_G(\sigma)}e_{\theta_G(\sigma)}(X).
 
\end{equation}
In particular every elementary coefficient of $\chi_G(X;q)$ belongs to
$\N[q]$. The assertion holds as a formal symmetric-function identity,
uniformly in $n$ and $G$.

Other possible paper matches, closest wording first

  • Theorem 6.7 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: polynomial, witness, permutation, partition, interval, elementary and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: finite.
  • Corollary 5.9 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: expansion, positivity, natural, interval, elementary, graph and two more.
  • Proposition 2.2 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: natural, interval, graph and unit.
  • Corollary 1.2 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: integer, permutation, graph and theta.
  • Theorem 3.1 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: integers, part, elementary and unit. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: nonnegative and finite.
  • Proposition 2.3 of Elementary positivity of chromatic quasisymmetric functions. Words of the Lean statement, its names split into words, that also appear in the theorem: coloring.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

This configuration names no theorem to prove. An accepted Comparator run compares the selected definitions by name and type; it does not verify a theorem proof.

Definitions compared by name and type only (1): elementaryPositivityWitness. Their bodies come from OpenAI’s solution library.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 169’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

  • MathVet

    Finds the whole advertised result stated or implied Their term: “full”.

    The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record

    Their note: elementaryPositivityWitness n G : G.PermutationWitness (a def closed by sorry, not a theorem) must supply theta : {σ // G.Nondescent σ} → Nat.Partition n with ∀ r, G.chromatic r = Σ_σ C(X^(graphInversions σ)) * esymmPart (theta σ) in MvPolynomial (Fin r) ℕ[X]: an explicit ℕ[q]-positive e-expansion for every natural unit interval graph (stronger than bare positivity). Chromatic quasisymmetric function and Hessenberg-function graphs are the standard definitions.

  • Carlos Toledo’s cert-machine

    Finds the whole advertised result stated or implied Their term: “MATCHES”.

    The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

63 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 2 to its own declarations, 51 to Mathlib’s documentation. 9 declared names also link to the same declaration in OpenAI’s library. 3 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInamespace ElementaryPositivitystructure NaturalUnitIntervalGraph (n : ℕ) where  h : Fin n → Fin n  increasing : Monotone h  extensive : ∀ i, i ≤ h inamespace NaturalUnitIntervalGraphvariable {n : ℕ} (G : NaturalUnitIntervalGraph n)def Edge (i j : Fin n) : Prop :=  (i < j ∧ j ≤ G.h i) ∨ (j < i ∧ i ≤ G.h j)instance (i j : Fin n) : Decidable (G.Edge i j) :=  inferInstanceAs (Decidable ((_ ∧ _) ∨ (_ ∧ _)))def Nondescent (σ : Equiv.Perm (Fin n)) : Prop :=  ∀ i j : Fin n, i.val + 1 = j.val → σ j < σ i → G.Edge (σ i) (σ j)instance (σ : Equiv.Perm (Fin n)) : Decidable (G.Nondescent σ) :=  inferInstanceAs (Decidable (∀ i j : Fin n,    i.val + 1 = j.val → σ j < σ i → G.Edge (σ i) (σ j)))def graphInversions (σ : Equiv.Perm (Fin n)) : ℕ :=  (Finset.univ.filter fun ij : Fin n × Fin n =>    ij.1 < ij.2 ∧ σ ij.2 < σ ij.1 ∧ G.Edge (σ ij.1) (σ ij.2)).carddef Proper {r : ℕ} (f : Fin n → Fin r) : Prop :=  ∀ i j : Fin n, G.Edge i j → f i ≠ f jinstance {r : ℕ} (f : Fin n → Fin r) : Decidable (G.Proper f) :=  inferInstanceAs (Decidable (∀ i j : Fin n, G.Edge i j → f i ≠ f j))def coloringAscents {r : ℕ} (f : Fin n → Fin r) : ℕ :=  (Finset.univ.filter fun ij : Fin n × Fin n =>    ij.1 < ij.2 ∧ G.Edge ij.1 ij.2 ∧ f ij.1 < f ij.2).cardnoncomputable def chromatic (r : ℕ) : MvPolynomial (Fin r) (Polynomial ℕ) :=  ∑ f ∈ Finset.univ.filter (G.Proper (r := r)),    MvPolynomial.C (Polynomial.X ^ G.coloringAscents f) *      ∏ i : Fin n, MvPolynomial.X (f i)structure PermutationWitness where  theta : {σ : Equiv.Perm (Fin n) // G.Nondescent σ} → Nat.Partition n  expansion : ∀ r : ℕ, G.chromatic r =    ∑ σ : {σ : Equiv.Perm (Fin n) // G.Nondescent σ},      MvPolynomial.C (Polynomial.X ^ G.graphInversions σ.val) *        MvPolynomial.esymmPart (Fin r) (Polynomial ℕ) (theta σ)end NaturalUnitIntervalGraphend ElementaryPositivitydef elementaryPositivityWitness (n : ℕ)    (G : ElementaryPositivity.NaturalUnitIntervalGraph n) :    G.PermutationWitness := by  sorryend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Elementary positivity of chromatic quasisymmetric functions

Theorem (Elementary positivity and a permutation witness)

There is a deterministic terminating procedure which, given a natural unit interval graph G on [n] and \sigma\in D_G^0, returns a partition \theta_G(\sigma)\vdash n such that

\chi_G(X;q)=\sum_{\sigma\in D_G^0} q^{\ginv_G(\sigma)}e_{\theta_G(\sigma)}(X).

In particular every elementary coefficient of \chi_G(X;q) belongs to \N[q]. The assertion holds as a formal symmetric-function identity, uniformly in n and G.

Section 1, Introduction Read it in the paper TeX source, line 39
Show the TeX
There is a deterministic terminating procedure which, given a natural
unit interval graph $G$ on $[n]$ and $\sigma\in D_G^0$, returns a partition
$\theta_G(\sigma)\vdash n$ such that
\begin{equation}
 \chi_G(X;q)=\sum_{\sigma\in D_G^0}
       q^{\ginv_G(\sigma)}e_{\theta_G(\sigma)}(X).
 
\end{equation}
In particular every elementary coefficient of $\chi_G(X;q)$ belongs to
$\N[q]$. The assertion holds as a formal symmetric-function identity,
uniformly in $n$ and $G$.
Corollary (Young permutation modules in Hessenberg cohomology)

Let n\ge1, let h be as above with graph G=G(h), and let S\in M_n(\C) be regular semisimple. Write

\operatorname{Hess}(S,h)= \{F_\bullet\in\operatorname{Flag}(\C^n): SF_i\subseteq F_{h(i)}\text{ for all }i\}.

For \lambda=(\lambda_1,\ldots,\lambda_\ell)\vdash n, let M^\lambda=\operatorname{Ind}_{S_\lambda}^{S_n}\mathbf{1}_{\C} be the Young permutation module, where S_\lambda=S_{\lambda_1}\times\cdots\times S_{\lambda_\ell} is the standard Young subgroup, and put

m_{\lambda,d}(h)= \#\{\sigma\in D_G^0:\theta_G(\sigma)=\lambda,\ \ginv_G(\sigma)=d\}.

Then for every integer d\ge0, under Tymoczko’s dot action on ordinary cohomology there is an abstract \C[S_n]-module isomorphism

H^{2d}(\operatorname{Hess}(S,h);\C) \cong\bigoplus_{\lambda\vdash n}(M^\lambda)^{\oplus m_{\lambda,d}(h)}.
Section 1, Introduction Read it in the paper TeX source, line 159
Show the TeX
Let $n\ge1$, let $h$ be as above with graph $G=G(h)$, and let
$S\in M_n(\C)$ be regular semisimple. Write
\[
 \operatorname{Hess}(S,h)=
 \{F_\bullet\in\operatorname{Flag}(\C^n):
     SF_i\subseteq F_{h(i)}\text{ for all }i\}.
\]
For $\lambda=(\lambda_1,\ldots,\lambda_\ell)\vdash n$, let
$M^\lambda=\operatorname{Ind}_{S_\lambda}^{S_n}\mathbf{1}_{\C}$ be the
Young permutation module, where
$S_\lambda=S_{\lambda_1}\times\cdots\times S_{\lambda_\ell}$ is the
standard Young subgroup, and put
\[
 m_{\lambda,d}(h)=
 \#\{\sigma\in D_G^0:\theta_G(\sigma)=\lambda,\ \ginv_G(\sigma)=d\}.
\]
Then for every integer $d\ge0$, under Tymoczko's dot action on ordinary
cohomology there is an abstract $\C[S_n]$-module isomorphism
\[
 H^{2d}(\operatorname{Hess}(S,h);\C)
 \cong\bigoplus_{\lambda\vdash n}(M^\lambda)^{\oplus m_{\lambda,d}(h)}.
\]
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 169 link it.
Solution module
OAI.Combinatorics.Chromatic.Main
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
12 local vocabulary declarations
Lines of Lean, without comments or blank lines
37
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Elementary positivity for natural unit interval graphs

Family 169: Shareshian–Wachs elementary positivity

Candidate pairing

Theorem (Elementary positivity and a permutation witness)

There is a deterministic terminating procedure which, given a natural unit interval graph G on [n] and \sigma\in D_G^0, returns a partition \theta_G(\sigma)\vdash n such that

\chi_G(X;q)=\sum_{\sigma\in D_G^0} q^{\ginv_G(\sigma)}e_{\theta_G(\sigma)}(X).

In particular every elementary coefficient of \chi_G(X;q) belongs to \N[q]. The assertion holds as a formal symmetric-function identity, uniformly in n and G.

Elementary positivity of chromatic quasisymmetric functions

TeX label main:theorem, build/sections/01-introduction.tex, line 39

The Lean statement says

def elementaryPositivityWitness (n : ℕ)    (G : ElementaryPositivity.NaturalUnitIntervalGraph n) :    G.PermutationWitness := by  sorry

Comparator checks only the name and type of elementaryPositivityWitness; its body comes from the solution.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.two independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

12 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/ElementaryPositivity.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

More about this statement

  • Commentary The review notes that the Lean statement leaves the rule as a definition hole that accepts any function meeting the expansion identity, so it states positivity but not the paper's explicit rule. Robert Joseph George, Do the Lean statements in openai/math match their papers?, 2026-10-07 Source
  • Commentary The post notes a definitional hole here but judges it acceptable, because the main objective is a data-carrying term rather than a proposition. Alex Meiburg, Several of the comparator challenges in the OpenAI release are broken and hackable, 2026-10-08 Source

Questions to resolve when comparing this statement with the paper

  • The configuration names no theorem: it checks a definition whose type carries the claim, so read that definition's type and body.
  • 1 definition hole: Comparator compares it by name and type only, so a reader checks what each solution body means.

Compare this statement with the paperShare a Comparator run reportSuggest a change