{"id":"palomar/PALOMAR-2026-11-01-000023","url":"https://github.com/jtraverso/kotzig-light-edges/tree/ccf55b1b968743ee5952ef4c9d78c88520f86bc2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000023-v2.json","repo":"https://github.com/jtraverso/kotzig-light-edges","tags":["math.CO","msc:05C10","msc:05C07","msc:52B10"],"score":0,"title":"Kotzig's theorem on light edges of planar graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Príspevok k teórii eulerovských polyédrov (Contribution to the theory of Eulerian polyhedra)","identifier":"Mat.-Fyz. Časopis Slovensk. Akad. Vied 5 (1955) 101–113","relationship":"formalizes"},{"title":"An introduction to the discharging method via graph coloring","identifier":"arXiv:1306.4434","relationship":"formalizes"},{"title":"On the total coloring of planar graphs","identifier":"doi:10.1515/crll.1989.394.180","relationship":"formalizes"},{"title":"Über den kartographischen Vierfarbensatz","identifier":"doi:10.1007/BF01444968","relationship":"formalizes"}]}