Erdős problem 593

Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.

Sources

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

593.lean

Retained formal statement4 of 10

Graph analogue — no odd cycle is obligatory (Erdős–Galvin–Hajnal [EGH75]): For every odd $k \geq 3$ , there exists a graph with chromatic cardinal $\aleph_1$ that contains no cycle of length $k$ . This shows the class of obligatory graphs is strictly smaller than all finite graphs.

FormalConjectures/ErdosProblems/593.leanErdos593.erdos_593.variants.graph_case_no_odd_cycle2 linesExact file

1True ↔2  ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ V G, G.chromaticCardinal = Cardinal.aleph 1 ∧ IsEmpty (SimpleGraph.cycleGraph k →g G)

SolvedStatement only, no proof