{"id":"palomar/PALOMAR-2026-10-16-000001","url":"https://github.com/jtraverso/hadwiger-mader/tree/a1ffd32233475c21ad474b2f80d57614911df9b0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000001-v2.json","repo":"https://github.com/jtraverso/hadwiger-mader","tags":["math.CO","msc:05C83","msc:05C15","msc:05C35"],"score":0,"title":"Mader's theorem and Hadwiger's conjecture for t ≤ 4","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Mader's theorem (a nonempty finite graph of average degree at least 2^(r−2) has a K_r minor), of Dirac's lemma (a graph without a K4 minor has a vertex of degree at most two, hence at most 2n − 3 edges for n ≥ 2), of Mader's bound for K5 (a graph on n ≥ 3 vertices with at least 3n − 5 edges has a K5 minor; equivalently, without a K5 minor it has at most 3n − 6 edges; added in version 2), and of Hadwiger's conjecture for t ≤ 4 (graphs without a K3 minor are 2-colourable, graphs without a K4 minor are 3-colourable). Minors are branch-set models.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"Homomorphieeigenschaften und mittlere Kantendichte von Graphen","identifier":"doi:10.1007/BF01364272","relationship":"formalizes"},{"title":"Homomorphiesätze für Graphen","identifier":"","relationship":"formalizes"},{"title":"A property of 4-chromatic graphs and some remarks on critical graphs","identifier":"doi:10.1112/jlms/s1-27.1.85","relationship":"formalizes"},{"title":"Über eine Klassifikation der Streckenkomplexe","identifier":"","relationship":"formalizes"}]}