Erdős Problem 923

References:

• erdosproblems.com/923
• [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (1969), 27-35.
• [Ro77] Rödl, V., On the chromatic number of subgraphs of a given graph. Proc. Amer. Math. Soc. (1977), 370-371.

theorem Erdos923.erdos_923 : True ↔ ∀ (V : Type u_1) (n : ℕ), ∃ (k : ℕ), ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3

Is it true that, for every $k$, there is some $f(k)$ such that if $G$ has chromatic number $\geq f(k)$ then $G$ contains a triangle-free subgraph with chromatic number $\geq k$?

This is true, as shown by Rödl [Ro77].