Erdős problem 918
A question of Erdős and Hajnal [ErHa68b], who proved that for every finite there is a graph with chromatic number and vertices where each subgraph on less than vertices has chromatic number .
Sources
FormalConjectures/ErdosProblems/
918.lean
Retained formal statement
A question of Erdős and Hajnal [ErHa68b], who proved that for every finite there is a graph with chromatic number and vertices where each subgraph on less than vertices has chromatic number .
∀ (k : ℕ), 0 < k → ∃ V G, Cardinal.mk V = Cardinal.aleph ↑k ∧ G.chromaticCardinal = Cardinal.aleph 1 ∧ ∀ (W : Set V), Cardinal.mk ↑W < Cardinal.aleph ↑k → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0SolvedStatement only, no proof