{"id":"palomar/PALOMAR-2026-10-16-000001","url":"https://github.com/jtraverso/hadwiger-mader/tree/cb10154cd439a419d0bbf34052839dd27242b619","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000001-v1.json","repo":"https://github.com/jtraverso/hadwiger-mader","tags":["math.CO","msc:05C83","msc:05C15","msc:05C35","graph-theory","hadwiger-conjecture","formal-verification","lean"],"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), 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-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Homomorphieeigenschaften und mittlere Kantendichte von Graphen","identifier":"doi:10.1007/BF01364272","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"}]}