Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Counterexamples to Hadwiger's conjecture

The binary frame construction yields arbitrarily large graphs with independence number at most two and small touching matchings. The matching–minor inequality then separates their complete-minor order from their ordinary chromatic number.

This formalizes the construction theorem and the ordinary chromatic consequence in OpenAI, A counterexample to Hadwiger's conjecture (September 23, 2026).

def OAI.HadwigerCounterexample.conflictLowerBound line 27
theorem OAI.HadwigerCounterexample.eventual_conflict_lower_bound line 32
theorem OAI.HadwigerCounterexample.exists_graphs line 66
Source documentation
Arbitrarily large finite graphs of independence number at most two and touching-matching number less than one hundredth of the number of vertices.
```
theorem exists_graphs (M : ℕ) : ∃ m:ℕ, max M 5 ≤ m ∧
    ∃ G : SimpleGraph (Fin m), G.indepNum ≤ 2 ∧
      (connectedMatchingNumber G:ℚ) < (m:ℚ)/100 := by
…
```

theorem OAI.HadwigerCounterexample.exists_counterexamples line 101

Source documentation

Arbitrarily large counterexamples to Hadwiger's conjecture, with the full rational bounds and finiteness of the ordinary chromatic number.

Distinct definitions of this name: ComparatorChallenges/HadwigerCounterexample.lean:38 (same statement text; different proof or body). Qualify references as OAI.HadwigerCounterexample.exists_counterexamples@path.

theorem exists_counterexamples (M : ℕ) : ∃ m : ℕ, max M 5 ≤ m ∧
    ∃ G : SimpleGraph (Fin m), G.indepNum ≤ 2 ∧ (connectedMatchingNumber G : ℚ) < (m : ℚ) / 100 ∧
      (hadwigerNumber G : ℚ) < 26 * (m : ℚ) / 75 + 2 / 3 ∧
      26 * (m : ℚ) / 75 + 2 / 3 < (m : ℚ) / 2 ∧ (m : ℚ) / 2 ≤ (G.chromaticNumber.toNat : ℚ) ∧
      hadwigerNumber G < G.chromaticNumber.toNat ∧
      G.chromaticNumber ≠ ⊤ ∧ G.chromaticNumber = ↑(G.chromaticNumber.toNat) := by
…

theorem OAI.HadwigerCounterexample.not_hadwiger_conjecture line 120
Distinct definitions of this name: ComparatorChallenges/HadwigerCounterexample.lean:49 (different declaration text). Qualify references as OAI.HadwigerCounterexample.not_hadwiger_conjecture@path.