{"id":"palomar/PALOMAR-2026-10-13-000005","url":"https://github.com/jtraverso/grotzsch-ore/tree/ff6d5123c06e4c99bb6074e0a72e8be8d595eefa","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000005-v2.json","repo":"https://github.com/jtraverso/grotzsch-ore","tags":["math.CO","msc:05C15","msc:05C10","msc:05C35","graph-theory","graph-coloring","lean"],"score":0,"title":"Grötzsch's theorem, Ore's conjecture for k = 4 (Kostochka–Yancey) and the Grünbaum–Aksenov 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 results on 3-colourings of planar graphs. (1) Kostochka and Yancey's theorem, the case k = 4 of Ore's 1967 conjecture on the minimum number of edges of k-critical graphs: every finite 4-critical graph G satisfies 3|E(G)| ≥ 5|V(G)| - 2, by their potential method. (2) Grötzsch's theorem: every finite triangle-free planar graph is 3-colourable, deduced from (1) as in Kostochka–Yancey, with the topological crossing argument replaced by a K5-minor argument with an apex inside a face. (3) Aksenov's and Jensen–Thomassen's theorem: a triangle-free planar graph…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Ore's conjecture for k = 4 and Grötzsch's theorem","identifier":"arXiv:1209.1173","relationship":"formalizes"},{"title":"Short proofs of coloring theorems on planar graphs","identifier":"arXiv:1211.3981","relationship":"formalizes"},{"title":"Zur Theorie der diskreten Gebilde, VII: Ein Dreifarbensatz für dreikreisfreie Netze auf der Kugel","identifier":"","relationship":"formalizes"},{"title":"Grötzsch's theorem on 3-colorings","identifier":"","relationship":"formalizes"},{"title":"On continuation of 3-colouring of planar graphs (Russian)","identifier":"","relationship":"formalizes"}]}