Formal target: Corpus.Hadwiger.conjecture
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.
Exact formal statement
∀ (t : Nat) {V : Type} [Fintype.{0} V] (G : SimpleGraph.{0} V),
Not (Corpus.Hadwiger.HasMinor G Top.top.{0}) → SimpleGraph.Colorable.{0} G (HSub.hSub.{0, 0, 0} t 1)This target is a formal statement, not a proof of the problem.
Environment availability: available.