Kuratowski's theorem
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000018
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000018/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-15-000018/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'