{"id":"palomar/PALOMAR-2026-11-04-000001","url":"https://github.com/jtraverso/kostochka-thomason-minors/tree/c7ddf34b1e4f9ba71932003c91176e2e6bb92d9f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000001-v1.json","repo":"https://github.com/jtraverso/kostochka-thomason-minors","tags":["math.CO","msc:05C83","msc:05C35","msc:05C80"],"score":0,"title":"Complete minors and average degree (Kostochka–Thomason)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Kostochka–Thomason theorem, following the short proof of Alon, Krivelevich and Sudakov. complete_minor_of_edges (their Theorem 1): there is d0 such that for every integer d ≥ d0, every nonempty finite simple graph with at least d·|V| edges has the complete graph K_t as a minor for every natural number t ≤ d / (10 √(ln d)). kostochka_thomason: there is a constant c > 0 such that for every integer d ≥ 2, every nonempty finite simple graph with at least d·|V| edges (average degree at least 2d) has a K_t minor for every t ≤ c·d / √(ln d). Minors are…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"Complete minors and average degree – a short proof","identifier":"arXiv:2202.08530","relationship":"formalizes"},{"title":"A lower bound for the Hadwiger number of graphs by their average degree","identifier":"","relationship":"formalizes"},{"title":"An extremal function for contractions of graphs","identifier":"","relationship":"formalizes"}]}