Arbitrarily large counterexamples to Hadwiger’s conjecture

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.

Do family 157’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.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

• MathVet

  Finds part of it stated, or a narrower or weaker statement Their term: “partial”.

  Only a special case is stated, or a co-equal headline claim has no challenge statement. Their record

  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 at 01-introduction.tex:58-67), 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

• Carlos Toledo’s cert-machine

  Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — DECLARED”.

  The challenge statements state less than the headline, and OpenAI’s Lean note says so. Their record

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

Read the complete assessments on the family page.