chromatic_polynomial_zeros_conjecture
Provedalgebragraph-theory
Chromatic polynomial: The chromatic polynomial P_G(k) counts proper k-colorings of G. Its zeros in ℂ are constrained; the region |z-1| ≤ 1 is conjectured to be zero-free (Sokal 2001). Many open questions on zero distribution.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem chromatic_polynomial_zeros_conjecture
(n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
∃ (P : Polynomial ℤ),
∀ k : ℤ, 0 ≤ k →
(P.eval k).toNat = {col : Fin n → Fin k.toNat |
∀ v w : Fin n, G.Adj v w → col v ≠ col w}.ncard := by
sorrySource