{"id":"palomar/PALOMAR-2026-10-15-000005","url":"https://github.com/jtraverso/planar-list-colouring/tree/ec1eafbc091713857eb5683a46e460902b2d47b3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000005-v1.json","repo":"https://github.com/jtraverso/planar-list-colouring","tags":["math.CO","msc:05C10","msc:05C15","msc:05C83","graph-theory","planar-graphs","list-coloring"],"score":0,"title":"Wagner's planarity criterion and list colouring of planar and K5-minor-free graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of classical results on planar graphs and graphs without a K5 minor. (1) Wagner's theorem (1937): a finite graph is planar if and only if it has neither K5 nor K3,3 as a minor. (2) Škrekovski's theorem (1998): every finite graph without a K5 minor is 5-choosable, proved along the route of Wood and Linusson, and Thomassen's theorem (1994) that every finite planar graph is 5-choosable, as a corollary. (3) DP-colouring: every finite graph without a K5 minor (Li–Wang, 2022), hence every finite planar graph (Dvořák–Postle, 2018), is DP-5-colourable. (4) Voigt's…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Über eine Eigenschaft der ebenen Komplexe","identifier":"","relationship":"formalizes"},{"title":"Choosability of K5-minor-free graphs","identifier":"doi:10.1016/S0012-365X(98)00158-7","relationship":"formalizes"},{"title":"Thomassen's Choosability Argument Revisited","identifier":"arXiv:1005.5194","relationship":"formalizes"},{"title":"Every planar graph is 5-choosable","identifier":"","relationship":"formalizes"},{"title":"Correspondence coloring and its application to list-coloring planar graphs without cycles of lengths 4 to 8","identifier":"","relationship":"formalizes"}]}