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