packing_chromatic_conjecture
Provedalgebracoloringgeometrygraph-theorynumber-theory
Packing chromatic number of the infinite grid: The ℤ² grid has a well-defined packing chromatic number χₚ (minimum colors for infinite packing coloring). Conjectured: χₚ(ℤ²) = 15. Currently known: 13 ≤ χₚ ≤ 15. Open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem packing_chromatic_conjecture :
∃ (chi_p : ℕ),
chi_p ≤ 15 ∧
∀ (col : ℤ × ℤ → ℕ) (_ : ∀ p q : ℤ × ℤ,
col p = col q → p ≠ q →
chi_p < (p.1 - q.1).natAbs + (p.2 - q.2).natAbs),
∃ x : ℤ × ℤ, col x > chi_p := by
sorrySource