Lax Lean Archive

Hadwiger's Conjecture for t = 7

lax-332265·formalized by Clemens Kuske @clemenskuske · Codex (OpenAI)·registered·created ·GitHub @f2bb3dd·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    Hadwiger's conjecture at t=7t=7 asserts that every finite graph with no K7K_7 minor is 6-colourable. This is the first unresolved case of the conjecture: the cases through t=6t=6 are known.

    The submission defines 6-colourability as the existence of a proper vertex colouring with six colours. It reuses, without alteration, the connected branch-set definition of a graph minor from the Planar Graph Classes submission (Lax68). Its sole theorem concept states the conjecture for finite graphs on canonical vertex types and deliberately has no proof, so the archive presents it as an open problem.

    Promising intermediate directions include imposing a bound on the independence number, forbidding additional induced subgraphs, or requiring a special decomposition. Recent general structural bounds improve the best known colouring bound for graphs with no KtK_t minor to O(tlog⁡log⁡log⁡t)O(t\log\log\log t), but they do not settle the six-colour bound at t=7t=7.

    Concepts

    Concept map
    3 concepts
    100%
    Open claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    No proofs in this submission.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-332265,
  author = {Clemens Kuske and Codex (OpenAI)},
  title = {Hadwiger's Conjecture for t = 7},
  year = {2026},
  howpublished = {Lax Archive, lax-332265},
  url = {https://laxarchive.org/lax-332265/},
}

    References

    1. Hugo Hadwiger. Über eine Klassifikation der Streckenkomplexe. Vierteljahrsschrift der Naturforschenden Gesellschaft in Zürich 88:133–142, 1943.
    2. Chun-Hung Liu and Jason Luo. Beyond Halfway to Hadwiger's Conjecture. 2026. doi:10.48550/arXiv.2609.06867 · arXiv:2609.06867

    Discussion

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

    Loading discussion…