{"id":"palomar/PALOMAR-2026-10-16-000003","url":"https://github.com/jtraverso/brooks/tree/b99e6f500256586626396de9c2d6fd4d96119d60","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000003-v2.json","repo":"https://github.com/jtraverso/brooks","tags":["math.CO","msc:05C15","msc:05C40","graph-coloring","graph-theory","formal-verification","lean"],"score":0,"title":"Brooks' theorem, degree-choosability and blocks","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Brooks' theorem: for k ≥ 3, a finite graph of maximum degree at most k without a (k+1)-clique is k-colourable (no connectedness assumption), and a finite connected graph that is neither complete nor an odd cycle is colourable with as many colours as its maximum degree. The proof uses greedy colourings in Lovász's style and an induction on the number of edges with a separation-and-gluing step. Version 2 adds the Erdős–Rubin–Taylor / Borodin theorem (a finite connected graph is degree-choosable, i.e. colourable from any lists with |L(v)| ≥ deg(v), if and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"On colouring the nodes of a network","identifier":"doi:10.1017/S030500410002168X","relationship":"formalizes"},{"title":"Choosability in graphs","identifier":"","relationship":"formalizes"},{"title":"Criteria of chromaticity of a degree prescription","identifier":"","relationship":"formalizes"},{"title":"Vertex colorings with given colors","identifier":"","relationship":"formalizes"}]}