Galvin's theorem, the Dinitz problem and stable matchings
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-18-000029
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000029/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-10-18-000029/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'