{"id":"palomar/PALOMAR-2026-10-18-000029","url":"https://github.com/jtraverso/galvin-dinitz/tree/0aa98fc17e1e96ec408f7bad3198ce37a08d26fc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000029-v1.json","repo":"https://github.com/jtraverso/galvin-dinitz","tags":["math.CO","msc:05C15","msc:05C70","msc:91B68","edge-colouring","stable-matching","lean"],"score":0,"title":"Galvin's theorem, 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 that the list chromatic index of a finite bipartite graph equals its maximum degree (if every edge has a list of at least Δ colours, a proper edge colouring can be chosen from the lists), of its corollary solving the Dinitz problem (an n × n array with lists of n symbols per cell admits a choice with distinct symbols in every row and column), and of the Gale–Shapley theorem on the existence of stable matchings with strict preferences and incomplete acceptability lists, which provides the kernels in Galvin's argument. Mathlib has line…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"The List Chromatic Index of a Bipartite Multigraph","identifier":"doi:10.1006/jctb.1995.1011","relationship":"formalizes"},{"title":"College Admissions and the Stability of Marriage","identifier":"doi:10.1080/00029890.1962.11989827","relationship":"formalizes"}]}