Graph coloring, clique minors, and Colin de Verdière invariants

MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).

Their note: HadwigerCounterexample states, for every M, a graph on Fin m with m >= max M 5, indepNum <= 2 and h(G) < 26m/75+2/3 < m/2 <= chi(G); the first-named claim follows by the routine bound chi_f(G) >= |V(G)|/alpha(G) >= m/2 (sum the vertex constraints of a fractional colouring; the paper does exactly this), although chi_f itself is not defined in the Lean. The summary’s co-equal second claim ('Also disproves’ the fractional Colin de Verdiere bound chi_f(G) <= mu(G)+1, the subject of a separate paper with a separate matrix-rank argument) has no challenge statement: no mu, well-signed matrix or Strong Arnold Property appears in either file. The positive list-colouring claim is stated verbatim by ListHadwiger.

Definitions the group asks readers to compare with the paper: HasCliqueMinor: t branch sets B : Fin t -> Set V, each nonempty and connected in G.induce (Mathlib’s Connected includes Nonempty), pairwise disjoint and pairwise joined by an edge; the standard K_t-minor definition; hadwigerNumber: sSup {t | HasCliqueMinor G t}, the largest clique-minor order h(G); the set is bounded by |V| for the finite V used (Fin m, Fintype V), so sSup is a true max; standard; IsTouchingMatching / connectedMatchingNumber: sets of 2-element cliques (edges), pairwise disjoint and pairwise joined by an edge between their endpoint sets, maximised via sSup; the paper’s ‘connected matching’ (cm), standard for this paper; listChromaticNumber: sInf {k | Choosable G k} with Choosable quantifying over every Color : Type and every list assignment of size >= k; the standard list chromatic number for finite G (set contains |V|, so sInf is the true minimum); junk value 0 for infinite G is excluded by [Fintype V] in MainStatement; MainStatement: a Prop-valued def, the type of main_theorem; exists C : N with 1 <= C chosen before V and G, so C is universal; [Fintype V] [Nonempty V] restrict to finite nonempty graphs as in the paper; standard; G.indepNum and G.chromaticNumber (Mathlib): standard; the statement adds chromaticNumber != top and chromaticNumber = ofNat(toNat) so the toNat casts are faithful; chi_f (fractional chromatic number): not defined anywhere in the Lean (Mathlib at the pinned revision has no such definition); the fractional form of the primary claim is recovered only outside Lean from alpha <= 2 and chi_f >= |V|/alpha

“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.

Their method: 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.

Read the original assessment Read MathVet’s method Details

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — DECLARED”).

The gap they name: The Colin de Verdière clause is not stated. The fractional clause is not stated as such (no χ_f), though it follows from the stated α ≤ 2 and h < m/2.

“NARROWER — DECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note says so.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method Details