Chapter 45, Theorem 3: high girth and chromatic number

Proved

BookSixth.high_girth_chromatic

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For every integer k at least 2, some finite simple graph is not properly k-colorable and has no simple cycle of length at most k. Thus its chromatic number and girth both exceed k.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.high_girth_chromatic (k : ℕ) (hk : 2 ≤ k) :
    ∃ N : ℕ, ∃ G : SimpleGraph (Fin N), ¬ HasColoring G k ∧
      ∀ l : ℕ, l ≤ k → ¬ HasCycle G l := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 45, Theorem 3: high girth and chromatic number, p. 314. https://doi.org/10.1007/978-3-662-57265-8_45

View graph