triangle_free_chromatic_number
Provedchromaticnumbercombinatoricsgraph-theorygraphtheorylogicnumber-theoryopen-problemproved
Triangle-free graphs with large chromatic number: For any k, triangle-free graphs with χ(G) ≥ k exist. Mycielski (1955) gave an explicit construction. Shows independence number and chromatic number are independent parameters.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem triangle_free_chromatic_number :
∀ k : ℕ, ∃ (n : ℕ) (G : SimpleGraph (Fin n)) (hD : DecidableRel G.Adj),
@SimpleGraph.chromaticNumber (Fin n) G ≥ k ∧
¬∃ a b c : Fin n, G.Adj a b ∧ G.Adj b c ∧ G.Adj a c := by
sorrySource