Borodin's light triangles in planar graphs of minimum degree five
A Lean 4 / Mathlib formalization of Borodin's theorem on light triangles, for finite simple graphs with the combinatorial planarity (genus-zero rotation systems) of the registered entry Kuratowski's theorem. The weight of a triangle is the sum of the degrees of its vertices. Every plane map of a graph of minimum degree at least five has a face of length three of weight at most 17 (light_face), and hence a planar graph of minimum degree at least five has a triangle of weight at most 17 (light_triangle). Two statements. The proof is a discharging argument run on the rotation system, with face…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000024
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000024/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-000024/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'