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
Erdős Problem 593 (500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number .
A natural conjectural characterization, recorded here, is that the obligatory finite 3-uniform hypergraphs are exactly the 2-colorable ones (Property B). The forward direction (IsObligatory → IsTwoColorable) and converse (IsTwoColorable → IsObligatory) are stated as separate variants below; in the graph case (), Erdős–Galvin–Hajnal [EGH75] proved the analogous result (obligatory ⇔ bipartite).
True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorableOpenStatement only, no proof