Kotzig's theorem on light edges of planar graphs
A Lean 4 / Mathlib formalization of Kotzig's theorem on light edges and its relatives, for finite simple graphs with the combinatorial planarity (genus-zero rotation systems) of the registered entry Kuratowski's theorem. The weight of an edge uv is deg u + deg v. A planar graph of minimum degree at least three has an edge of weight at most 13 (kotzig_borodin; the form without 3-connectivity conjectured by Erdős and proved by Borodin); a planar graph of minimum degree at least four has an edge of weight at most 11 (light_edge_minDegree_four); Kotzig's theorem (1955): a 3-connected planar…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000023
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000023/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-11-01-000023/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'