{"id":"palomar/PALOMAR-2026-10-15-000018","url":"https://github.com/jtraverso/kuratowski/tree/696ec897a9b91933037767d897670aa30ba3683a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000018-v1.json","repo":"https://github.com/jtraverso/kuratowski","tags":["math.CO","msc:05C10","msc:05C83","graph-theory","planarity","formal-verification","lean"],"score":0,"title":"Kuratowski's theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Kuratowski's theorem: a finite graph is planar if and only if it contains no subdivision of K5 and no subdivision of K3,3. Planarity is the combinatorial notion (a rotation system of genus zero). The proof combines Wagner's minor characterization (from the author's planarity library) with three new lemmas: a subdivision of any finite graph H gives H as a minor; a K3,3 minor gives a K3,3 subdivision; a K5 minor gives a K5 or a K3,3 subdivision. The last two rest on joining up to four terminals inside a connected branch set to one centre or to two adjacent…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Sur le problème des courbes gauches en Topologie","identifier":"doi:10.4064/fm-15-1-271-283","relationship":"formalizes"}]}