Erdős Problem 108

Reference: erdosproblems.com/108

theorem Erdos108.erdos_108 : True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ (f : ℕ), ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ (H : G.Subgraph), H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k

For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?