{"id":"palomar/PALOMAR-2026-10-28-000018","url":"https://github.com/jtraverso/pippenger-spencer/tree/4cca4e3c641619b1622ea60f58c57dc0c28ffdbb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000018-v1.json","repo":"https://github.com/jtraverso/pippenger-spencer","tags":["math.CO","math.PR","msc:05C65","msc:05C15","msc:05C70","msc:05D40"],"score":0,"title":"The Pippenger–Spencer theorem on the chromatic index of hypergraphs","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 theorem of Pippenger and Spencer (1989): for r ≥ 2 and ε > 0 there are μ > 0 and D₀ such that every r-uniform hypergraph whose degrees lie in [(1 − μ)D, D] and whose codegrees are at most μD, with D ≥ D₀, has chromatic index at most (1 + ε)D. A second theorem gives an explicit polynomial error: if the maximum degree is at most D, the codegrees are at most D^{1−δ} and there are at most exp(D^γ) edges, then the chromatic index is at most D + D^{1−γ} for some γ = γ(r, δ) > 0. The proofs build on the author's registered formalization of Ehard–Glock–Joos…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Asymptotic behavior of the chromatic index for hypergraphs","identifier":"doi:10.1016/0097-3165(89)90074-5","relationship":"formalizes"}]}