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
FormalConjectures/ErdosProblems/
593.lean
Retained formal statement
Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal must have an uncountable vertex set.
Proof: If V is countable, there exists an injection φ : V → ℕ. Using distinct natural numbers as colors gives a proper coloring, so , contradicting .
∀ {V : Type} (H : ThreeUniformHypergraph V), Cardinal.aleph0 < H.chromaticCardinal → ¬Countable VTextbookStatement only, no proof