Erdős Problem 594

References:

• erdosproblems.com/594
• [ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99.
• [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35.
• [EHS74] Erdős, P. and Hajnal, A. and Shelah, S., On some general properties of chromatic numbers. Topics in topology (Proc. Colloq., Keszthely, 1972) (1974), 243-255.

theorem Erdos594.erdos_594 : True ↔ ∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) → ∃ (N : ℕ), ∀ (k : ℕ), N ≤ k → ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = 2 * k + 1

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

theorem Erdos594.erdos_594.variants.erdos_hajnal (V : Type) (G : SimpleGraph V) (h : ∀ (α : Type), Cardinal.mk α ≤ Cardinal.aleph 1 → IsEmpty (G.Coloring α)) : ∃ (N : ℕ), ∀ (k : ℕ), N ≤ k → ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = 2 * k + 1

The earlier result of Erdős and Hajnal [ErHa66]: every graph with chromatic number $\geq \aleph_2$ contains all sufficiently large odd cycles.

Chromatic number $\geq \aleph_2$ is encoded as the nonexistence of a proper colouring with any set of at most $\aleph_1$ colours.

theorem Erdos594.erdos_594.variants.bot_countably_colorable : ¬IsEmpty (⊥.Coloring ℕ)

Sanity check for the encoding of "chromatic number $\geq \aleph_1$": a countably colourable graph, such as the empty graph on $\mathbb{N}$, does not satisfy the hypothesis IsEmpty (G.Coloring ℕ).