Source labels openChecked July 26, 2026

Erdős Problem 593

*Erdős Problem 593 ( $500)**: Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number$ > \aleph_0$.

Combinatorics AMS 5

Mathematical statement

*Erdős Problem 593 ( $500)**: Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number$ > \aleph_0$.

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 ( $r = 2$ ), Erdős–Galvin–Hajnal [EGH75] proved the analogous result (obligatory ⇔ bipartite).

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_593

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_593 : answer(sorry) ↔    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),      IsObligatory F ↔ F.IsTwoColorable := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/593background