{"id":"palomar/PALOMAR-2026-10-18-000029","url":"https://github.com/jtraverso/galvin-dinitz/tree/84dcda4c2a760f2b52b7e813affe7e6968f8bfce","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000029-v2.json","repo":"https://github.com/jtraverso/galvin-dinitz","tags":["math.CO","msc:05C15","msc:05C70","msc:91B68"],"score":0,"title":"Galvin's theorem for bipartite multigraphs, the Dinitz problem and stable matchings","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Galvin’s theorem for finite bipartite multigraphs: every assignment of finite edge lists of size at least the maximum incidence degree admits a proper edge coloring, with parallel edges counted separately. It includes ordinary edge coloring with Δ colors and the matching lower bound, and the Borodin–Kostochka–Woodall theorem for local lists (lists of size at least the larger degree of the two ends of each edge suffice). The previously registered simple-graph Galvin theorem, Dinitz problem and Gale–Shapley stable matching theorem are retained.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"The List Chromatic Index of a Bipartite Multigraph","identifier":"doi:10.1006/jctb.1995.1011","relationship":"formalizes"},{"title":"List Edge and List Total Colourings of Multigraphs","identifier":"doi:10.1006/jctb.1997.1780","relationship":"formalizes"},{"title":"College Admissions and the Stability of Marriage","identifier":"doi:10.1080/00029890.1962.11989827","relationship":"formalizes"}]}