{"id":"palomar/PALOMAR-2026-10-15-000019","url":"https://github.com/jtraverso/konig-edge-colouring/tree/7c60f7efb69c1747aaf39e5dfa7a89d907cd84ef","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000019-v1.json","repo":"https://github.com/jtraverso/konig-edge-colouring","tags":["math.CO","msc:05C15","msc:05C70","msc:06A07","graph-theory","edge-colouring","formal-verification","lean"],"score":0,"title":"Kőnig's theorems and Dilworth's theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Kőnig's edge-colouring theorem: the line graph of a finite bipartite graph G is Δ(G)-colourable, and its chromatic number (the chromatic index of G) equals Δ(G). The proof colours edges one at a time with partial proper edge colourings, recolouring by an a/b Kempe-chain swap whose correctness rests on a parity argument in the bipartite graph; the lower bound comes from the edges at a vertex of maximum degree, which are pairwise adjacent in the line graph. Also formalized: the Kőnig–Egerváry theorem (a finite bipartite graph has a matching and a vertex…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre","identifier":"doi:10.1007/BF01456961","relationship":"formalizes"},{"title":"Gráfok és mátrixok","identifier":"","relationship":"formalizes"},{"title":"A decomposition theorem for partially ordered sets","identifier":"doi:10.2307/1969503","relationship":"formalizes"},{"title":"A dual of Dilworth's decomposition theorem","identifier":"doi:10.1080/00029890.1971.11992886","relationship":"formalizes"}]}