Erdős Problem #594

**Erdős Problem 594** (Erdős–Hajnal [ErHa66], [Er69b]): Does every graph \(G\) with chromatic number \(\geq \aleph_1\) contain all sufficiently large odd cycles? The answer is **Yes**, proved by Erdős, Hajnal, and Shelah [EHS74]. A graph has chromatic number \(\geq \aleph_1\) (i.e. uncountable chromatic number) if and only if it admits no proper colouring with countably many colours; this is encoded as `IsEmpty (G.Coloring ℕ)`. The conclusion states that there is some \(N\) such that for every \(k \geq N\) the graph contains a cycle of odd length \(2k + 1\).