{"id":"palomar/PALOMAR-2026-10-16-000015","url":"https://github.com/jtraverso/gallai-roy/tree/e737218bf80c3d3684d670f5f8aa9a8257e1a52f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000015-v1.json","repo":"https://github.com/jtraverso/gallai-roy","tags":["math.CO","msc:05C15","msc:05C20","graph-theory","graph-coloring","formal-verification","lean"],"score":0,"title":"The Gallai–Hasse–Roy–Vitaver 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 the Gallai–Hasse–Roy–Vitaver theorem: if an orientation of a finite graph has no directed path on more than k vertices, the graph is k-colourable; and conversely every k-colourable graph has such an orientation. Hence the chromatic number is the minimum over orientations of the number of vertices of a longest directed path.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Nombre chromatique et plus longs chemins d'un graphe","identifier":"doi:10.1051/m2an/1967010501291","relationship":"formalizes"},{"title":"Zur algebraischen Begründung der Graphentheorie. I","identifier":"doi:10.1002/mana.19650280503","relationship":"formalizes"},{"title":"On directed paths and circuits","identifier":"","relationship":"formalizes"},{"title":"Determination of minimal coloring of vertices of a graph by means of Boolean powers of the incidence matrix","identifier":"","relationship":"formalizes"}]}