Erdős problem 1175
Let be an uncountable cardinal. Must there exist a cardinal such that every graph with chromatic number contains a triangle-free subgraph with chromatic number ?
Sources
FormalConjectures/ErdosProblems/
1175.lean
Retained formal statement
Let be an uncountable cardinal. Must there exist a cardinal such that every graph with chromatic number contains a triangle-free subgraph with chromatic number ?
Shelah proved that a negative answer is consistent when (see erdos_1175.variants.shelah_consistency).
True ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ μ, ∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κOpenStatement only, no proof