{"id":"palomar/PALOMAR-2026-10-19-000013","url":"https://github.com/jtraverso/alon-tarsi-choosability/tree/4ab98b11f340ea2160b34d0b57ef7102452b98cc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000013-v1.json","repo":"https://github.com/jtraverso/alon-tarsi-choosability","tags":["math.CO","msc:05C15","msc:05C10","msc:05C20","graph-theory","list-coloring","formalization"],"score":0,"title":"The Alon–Tarsi theorem and 3-choosability of planar bipartite graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Alon–Tarsi theorem: if a finite simple graph has an orientation whose numbers of even and odd Eulerian subdigraphs differ, then it can be properly coloured from any lists larger than the out-degrees; and of its corollary that every finite planar bipartite graph is 3-choosable. Planarity is the combinatorial notion of a plane map (a rotation system of genus zero) of the registered entry PALOMAR-2026-10-15-000005, whose definitions are reproduced verbatim in the Challenge. The proof uses the graph polynomial and Mathlib's Combinatorial Nullstellensatz,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Colorings and orientations of graphs","identifier":"doi:10.1007/BF01204715","relationship":"formalizes"}]}