Lax Lean Archive

Hadwiger's conjecture for t = 7

Lax332265.HadwigerT7 · concepts/Lax332265/HadwigerT7.lean · lax-332265

open

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Opn

    Every finite graph with no K₇ minor is 6-colourable. This is the first open case of Hadwiger's conjecture.

    Concept map
    3 concepts
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    Lean source view on GitHub

    1import Lax68.GraphMinors
    2import Lax332265.SixColorable
    3
    4/-!
    5---
    6title: Hadwiger's conjecture for t = 7
    7type: opn
    8---
    9Every finite graph with no *K*₇ minor is 6-colourable. This is the first open
    10case of Hadwiger's conjecture.
    11
    12# Formalization notes
    13
    14Finite graphs are stated on the canonical carriers `Fin n`. The complete
    15seven-vertex graph is written directly as `SimpleGraph.completeGraph (Fin 7)`;
    16introducing a named abbreviation would add no reusable notion beyond the
    17existing complete-graph construction.
    18
    19The minor relation is exactly `Lax68.GraphMinors.IsMinor` from the Planar
    20Graph Classes submission: a minor model consists of pairwise disjoint,
    21connected branch sets, with an edge between the appropriate branch sets for
    22every edge of the modeled graph. Six-colourability is the separate definition
    23introduced by this submission.
    24
    25# Research directions
    26
    27Potential intermediate cases add structure to the excluded-minor hypothesis,
    28for example by bounding the independence number, excluding specified induced
    29subgraphs, or requiring a special graph decomposition. These strengthen the
    30hypotheses but leave the conclusion unchanged.
    31-/
    32
    33namespace Lax332265.HadwigerT7
    34
    35/-- Hadwiger's conjecture at `t = 7`: excluding a `K₇` minor guarantees a
    36proper colouring with six colours. -/
    37axiom sixColorable_of_no_K7_minor :
    38 ∀ (n : ℕ) (G : SimpleGraph (Fin n)),
    39 ¬ Lax68.GraphMinors.IsMinor
    40 (SimpleGraph.completeGraph (Fin 7)) G →
    41 Lax332265.SixColorable.IsSixColorable G
    42
    43end Lax332265.HadwigerT7
    44
    Formalization notes

    Finite graphs are stated on the canonical carriers FinnFin n. The complete seven-vertex graph is written directly as SimpleGraph.completeGraph(Fin7)SimpleGraph.completeGraph (Fin 7); introducing a named abbreviation would add no reusable notion beyond the existing complete-graph construction.

    The minor relation is exactly Lax68.GraphMinors.IsMinorLax68.GraphMinors.IsMinor from the Planar Graph Classes submission: a minor model consists of pairwise disjoint, connected branch sets, with an edge between the appropriate branch sets for every edge of the modeled graph. Six-colourability is the separate definition introduced by this submission.

    Research directions

    Potential intermediate cases add structure to the excluded-minor hypothesis, for example by bounding the independence number, excluding specified induced subgraphs, or requiring a special graph decomposition. These strengthen the hypotheses but leave the conclusion unchanged.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…