{"id":"palomar/PALOMAR-2026-10-18-000016","url":"https://github.com/jtraverso/spectral-graph-bounds/tree/8d8b4ce17e56165b5f1ad3b285fb141666804e1c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000016-v1.json","repo":"https://github.com/jtraverso/spectral-graph-bounds","tags":["math.CO","msc:05C50","msc:05C15","msc:05C69","spectral-graph-theory","chromatic-number","lean"],"score":0,"title":"Spectral bounds on the chromatic and independence numbers","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of classical eigenvalue bounds for a finite simple graph G on a nonempty vertex type, with λ_max and λ_min the largest and smallest eigenvalues of its real adjacency matrix: the average degree is at most λ_max and λ_max is at most the maximum degree (Collatz–Sinogowitz); G is (⌊λ_max⌋ + 1)-colourable (Wilf 1967); if G has an edge, every proper colouring uses at least 1 − λ_max/λ_min colours (Hoffman 1970); and if G is k-regular with k ≥ 1, every independent set has at most n(−λ_min)/(k − λ_min) vertices (Hoffman's ratio bound). Mathlib has the spectral…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"Spektren endlicher Grafen","identifier":"doi:10.1007/BF02941924","relationship":"formalizes"},{"title":"The Eigenvalues of a Graph and Its Chromatic Number","identifier":"doi:10.1112/jlms/s1-42.1.330","relationship":"formalizes"},{"title":"On eigenvalues and colorings of graphs","identifier":"","relationship":"formalizes"}]}