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
Conjunction of the two open implications gives the conjectured characterization: if both obligatory_implies_two_colorable and two_colorable_implies_obligatory hold, then the characterization conjectured in erdos_593 (IsObligatory F ↔ F.IsTwoColorable) follows by elementary Iff manipulation.
(∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorable) → (∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F) → ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorableTestStatement only, no proof