{"id":"palomar/PALOMAR-2026-10-15-000004","url":"https://github.com/jtraverso/vizing/tree/01c72ed7efde2353a4bb1654f69b5c0bc5038863","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000004-v1.json","repo":"https://github.com/jtraverso/vizing","tags":["math.CO","msc:05C15","graph-theory","edge-coloring","formal-verification"],"score":0,"title":"Vizing's theorem and equitable edge colourings","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Vizing's theorem: every finite simple graph G has a proper edge colouring with Δ(G) + 1 colours, stated with Mathlib's line graph (G.lineGraph is (Δ(G) + 1)-colourable, hence χ'(G) ≤ Δ(G) + 1), proved with fans and Kempe chain exchanges. It also proves the equitable refinement: for every c ≥ Δ(G) + 1 there is a proper edge colouring with colours Fin c in which any two colour classes (including unused colours) differ in size by at most one (McDiarmid 1972), obtained by balancing a Vizing colouring with alternating-component moves that strictly decrease a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"On an estimate of the chromatic class of a p-graph (Russian)","identifier":"","relationship":"formalizes"},{"title":"The Solution of a Timetabling Problem","identifier":"doi:10.1093/imamat/9.1.23","relationship":"formalizes"}]}