Grötzsch's theorem, Ore's conjecture for k = 4 (Kostochka–Yancey) and the Grünbaum–Aksenov theorem
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-13-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000005/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'