graph-theory · graph-colouring · graph-minors
For every integer t ≥ 1 and every finite simple graph G, if G cannot be coloured with t−1 colours so that adjacent vertices receive different colours, must G contain a K_t minor? Here a K_t minor means t nonempty, pairwise disjoint vertex sets, each inducing a connected graph, with an edge of G between every pair of sets. K_t is the complete graph on t vertices.
Why it matters
The conjecture connects a global colouring obstruction to a concrete structure built by contracting connected pieces. Its t = 5 case is equivalent to the four-colour theorem.
One possible first attack
Work out t = 3: show that a graph with no K₃ minor has no cycle, and construct a two-colouring of each tree component. Translate a cycle into three nonempty branch sets explicitly. This recovers a known case and tests the custom minor definition; it is not a route promised to handle t ≥ 7.
Mathematical status
Open in general; the cases t ≤ 6 are known, while t ≥ 7 remains unresolved in the cited research (checked 2026-09-11). The Lean target quantifies over all natural t; t = 0 adds only a vacuous case, since every graph has the empty minor.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Steiner, Hadwiger’s conjecture and topological bounds, introduction: finite graph statement, known t ≤ 6 cases, and open general problem (checked 2026-09-11): https://arxiv.org/abs/2312.17130
Local target: Corpus.Hadwiger.conjecture
Source SHA-256: 7c8bcbfc552e28221c16539e048a9cbcb3e3508839f9436517afe7efbcbcc8a4
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For every integer t ≥ 1 and every finite simple graph G, if G cannot be coloured with t−1 colours so that adjacent vertices receive different colours, must G contain a K_t minor? Here a K_t minor means t nonempty, pairwise disjoint vertex sets, each inducing a connected graph, wi
No public records on this page.
No public records on this page.