theorem HighGirthChromatic.induce_compl_no_short_cycles {n : ℕ} {G : SimpleGraph (Fin n)} [DecidableRel G.Adj] (S : Finset (Fin n)) (g : ℕ) (hS : ∀ (v : Fin n) (w : G.Walk v v), w.IsCycle → w.length ≤ g → ∃ u ∈ S, u ∈ w.support.toFinset) (v : ↑↑(Finset.univ \ S)) (w : (SimpleGraph.induce (↑(Finset.univ \ S)) G).Walk v v) : w.IsCycle → g < w.length

If every short cycle of $G$ (length $\leq g$) passes through some vertex of $S$, then the subgraph induced on $V \setminus S$ has girth strictly greater than $g$.

theorem HighGirthChromatic.erdos_probabilistic_argument (k g : ℕ) (hg : 2 < g) : ∃ (V : Type) (x : Fintype V) (G : SimpleGraph V) (x : DecidableRel G.Adj), ¬G.Colorable k ∧ g < G.girth

The probabilistic step of Erdős' construction: for every $k$ and every $g > 2$, there is a finite graph $G$ that is not $k$-colorable and has girth greater than $g$.

theorem HighGirthChromatic.exists_not_colorable_high_girth (k g : ℕ) : ∃ (V : Type) (x : Fintype V) (G : SimpleGraph V) (x : DecidableRel G.Adj), ¬G.Colorable k ∧ g < G.girth

For any $k$ and $g$, there exists a finite graph that is not $k$-colorable and whose girth exceeds $g$. The small-girth case ($g \leq 2$) is handled by a complete graph; the generic case reduces to erdos_probabilistic_argument.

theorem HighGirthChromatic.exists_high_girth_high_chromatic (k g : ℕ) : ∃ (V : Type) (x : Fintype V) (G : SimpleGraph V), ↑k < G.chromaticNumber ∧ g < G.girth

Theorem 3.4.1 (Erdős 1959). For all natural numbers $k$ and $g$, there exists a finite graph $G$ with girth strictly greater than $g$ and chromatic number strictly greater than $k$.