Erdős problem 923

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$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

923.lean

Retained formal statement1 of 1

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].

FormalConjectures/ErdosProblems/923.leanErdos923.erdos_9233 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.