From d3ac3c1459e041cc81d1ee21111f05f170a7479a Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Thu, 16 Apr 2026 13:23:25 +0100
Subject: [PATCH 1/7] feat(ErdosProblems/593): formalize obligatory 3-uniform
 subhypergraphs ($500 prize)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds formalization of Erdős Problem 593 (Erdős-Galvin-Hajnal, $500 prize).
Reference: https://www.erdosproblems.com/593

Characterize finite 3-uniform hypergraphs appearing in every 3-uniform
hypergraph of chromatic number > ℵ₀. Includes ThreeUniformHypergraph structure,
chromaticCardinal for hypergraphs, 4 fully proved lemmas, and graph analogue
variants. Assisted by Claude (Anthropic).
---
 FormalConjectures/ErdosProblems/593.lean | 265 +++++++++++++++++++++++
 1 file changed, 265 insertions(+)
 create mode 100644 FormalConjectures/ErdosProblems/593.lean

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
new file mode 100644
index 0000000000..37e97b8210
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -0,0 +1,265 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 593
+
+*Reference:* [erdosproblems.com/593](https://www.erdosproblems.com/593)
+
+*References for known results:*
+- [EGH75] Erdős, Paul and Galvin, Fred and Hajnal, András, On set-systems having large
+  chromatic number and not containing prescribed subsystems.
+  Infinite and finite sets (Colloq., Keszthely, 1973; dedicated to P. Erdős on his 60th
+  birthday), Vol. I. Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 425–513.
+- [Er95d] Erdős, Paul, Some of my favourite problems in various branches of combinatorics.
+  Matematiche (Catania) 47 (1992), no. 2, 231–240 (1995).
+
+**Problem (Erdős, $500)**: Characterize those finite 3-uniform hypergraphs which appear in
+every 3-uniform hypergraph of chromatic number $> \aleph_0$.
+
+**Background:** A hypergraph $H = (V, E)$ is **$r$-uniform** if every hyperedge $e \in E$
+has exactly $r$ vertices. The **chromatic number** $\chi(H)$ of a hypergraph is the minimum
+number of colors needed to color its vertices so that no hyperedge is monochromatic. A finite
+$r$-uniform hypergraph $F$ is **obligatory** (for the class of $r$-uniform hypergraphs with
+chromatic number $> \aleph_0$) if every $r$-uniform hypergraph with chromatic number
+$> \aleph_0$ contains a copy of $F$ as a sub-hypergraph.
+
+**Known (graph case, $r = 2$, Erdős–Galvin–Hajnal [EGH75]):** For graphs (2-uniform
+hypergraphs), the problem is completely solved:
+- A graph of chromatic number $\geq \aleph_1$ must contain all finite bipartite graphs.
+- No fixed odd cycle is obligatory: for every odd $k$, there exists a graph with chromatic
+  number $\aleph_1$ that contains no cycle of length $k$.
+
+The 3-uniform case remains **open**.
+
+**Formalization notes:** We represent a 3-uniform hypergraph on vertex type `V` as a pair
+`(edges, uniform)` where `edges : Set (Finset V)` and every edge has cardinality 3. A proper
+coloring sends vertices to colors such that no hyperedge is monochromatic. The chromatic
+cardinal is the infimum of cardinalities of color types admitting a proper coloring. A finite
+hypergraph `F` *appears* in `H` if there is an injective vertex map carrying edges of `F`
+into edges of `H`.
+
+We work at universe level `Type` (universe 0) throughout to avoid universe metavariable issues.
+-/
+
+open Cardinal Set SimpleGraph
+
+namespace Erdos593
+
+/- ## Definitions for 3-uniform hypergraphs -/
+
+/-- A **3-uniform hypergraph** on vertex type `V` is a set of 3-element `Finset`s.
+Each element of `edges` is a hyperedge, and `uniform` ensures each has exactly 3 vertices. -/
+structure ThreeUniformHypergraph (V : Type) where
+  /-- The set of hyperedges: each edge is a 3-element finset of vertices. -/
+  edges : Set (Finset V)
+  /-- Every hyperedge has exactly 3 vertices. -/
+  uniform : ∀ e ∈ edges, e.card = 3
+
+/-- A **proper coloring** of a 3-uniform hypergraph `H` by a color type `C` is a vertex
+coloring such that no hyperedge is monochromatic (all three vertices receive the same color). -/
+def ThreeUniformHypergraph.IsProperColoring {V : Type} (H : ThreeUniformHypergraph V)
+    {C : Type} (f : V → C) : Prop :=
+  ∀ e ∈ H.edges, ∃ u ∈ e, ∃ v ∈ e, f u ≠ f v
+
+/-- The **chromatic cardinal** of a 3-uniform hypergraph `H` is the infimum of cardinalities
+of color types admitting a proper coloring. We use `Cardinal.{0}` matching `Type`. -/
+noncomputable def ThreeUniformHypergraph.chromaticCardinal {V : Type}
+    (H : ThreeUniformHypergraph V) : Cardinal.{0} :=
+  sInf {κ : Cardinal.{0} | ∃ (C : Type), #C = κ ∧ ∃ f : V → C, H.IsProperColoring f}
+
+/-- A finite 3-uniform hypergraph `F` **appears** in `H` (as a sub-hypergraph) if there
+exists an injective vertex map `φ : W → V` that sends every hyperedge of `F` to a hyperedge
+of `H`. -/
+def ThreeUniformHypergraph.Appears {W V : Type} [DecidableEq V]
+    (F : ThreeUniformHypergraph W) (H : ThreeUniformHypergraph V) : Prop :=
+  ∃ φ : W → V, Function.Injective φ ∧
+    ∀ e ∈ F.edges, e.image φ ∈ H.edges
+
+/-- A finite 3-uniform hypergraph `F` on a `Fintype` vertex type is **obligatory** if it
+appears in every 3-uniform hypergraph (on a `Type`-valued vertex set) whose chromatic
+cardinal exceeds `ℵ₀`. -/
+def IsObligatory {W : Type} [Fintype W] (F : ThreeUniformHypergraph W) : Prop :=
+  ∀ (V : Type) [DecidableEq V] (H : ThreeUniformHypergraph V),
+    ℵ₀ < H.chromaticCardinal → F.Appears H
+
+/- ## Main open problem -/
+
+/--
+**Erdős Problem 593 ($500)**: Characterize those finite 3-uniform hypergraphs which appear in
+every 3-uniform hypergraph of chromatic number $> \aleph_0$.
+
+*Original statement (erdosproblems.com/593)*: "Characterize those finite 3-uniform hypergraphs
+which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$."
+
+**Background:** For graphs (2-uniform hypergraphs), the analogous problem is completely solved
+by Erdős, Galvin, and Hajnal [EGH75]: the obligatory finite graphs are precisely the finite
+bipartite graphs. No fixed odd cycle is obligatory. The 3-uniform case is open.
+
+**Formalization:** We express the problem as asking for a characterization predicate `P` for
+obligatory finite 3-uniform hypergraphs (formalized via `IsObligatory`). The `answer(sorry)`
+records that no such characterization is known.
+
+**Prize:** \$500 (see erdosproblems.com/593).
+
+**Status:** OPEN.
+-/
+@[category research open, AMS 5]
+theorem erdos_593 : answer(sorry) ↔
+    ∃ (P : ∀ (W : Type) [Fintype W], ThreeUniformHypergraph W → Prop),
+      ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+        IsObligatory F ↔ P W F := by
+  sorry
+
+/- ## Variants and partial results -/
+
+/--
+**Graph analogue — bipartite graphs are obligatory (solved, Erdős–Galvin–Hajnal [EGH75])**:
+For the 2-uniform (graph) case, a graph of chromatic cardinal $> \aleph_0$ must contain all
+finite bipartite graphs. Specifically, for every finite bipartite graph `F` and every graph
+`G` with chromatic cardinal $> \aleph_0$, there is a graph homomorphism from `F` to `G`.
+
+**Status:** SOLVED [EGH75].
+-/
+@[category research solved, AMS 5]
+theorem erdos_593.variants.graph_case_bipartite_obligatory :
+    answer(True) ↔
+    ∀ (V : Type*) (G : SimpleGraph V),
+      ℵ₀ < G.chromaticCardinal →
+      ∀ (W : Type*) [Fintype W] (F : SimpleGraph W), F.IsBipartite →
+        Nonempty (F →g G) := by
+  simp only [true_iff]
+  -- This is the Erdős–Galvin–Hajnal theorem [EGH75].
+  sorry
+
+/--
+**Graph analogue — no odd cycle is obligatory (solved, 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.
+
+**Status:** SOLVED [EGH75].
+-/
+@[category research solved, AMS 5]
+theorem erdos_593.variants.graph_case_no_odd_cycle :
+    answer(True) ↔
+    ∀ k : ℕ, Odd k → 3 ≤ k →
+      ∃ (V : Type*) (G : SimpleGraph V),
+        G.chromaticCardinal = ℵ_ 1 ∧
+        IsEmpty (cycleGraph k →g G) := by
+  simp only [true_iff]
+  -- This is the Erdős–Galvin–Hajnal theorem [EGH75].
+  sorry
+
+/--
+**Vertices must be uncountable**: Every 3-uniform hypergraph with chromatic cardinal
+$> \aleph_0$ 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 $\chi(H) \leq \#\mathbb{N} = \aleph_0$,
+contradicting $\chi(H) > \aleph_0$.
+-/
+@[category undergraduate, AMS 5]
+theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
+    {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
+    ¬ Countable V := by
+  intro hcount
+  -- Since V is countable, there is an injection φ : V → ℕ.
+  obtain ⟨φ, hφ⟩ := Countable.exists_injective_nat V
+  -- The injection φ is a proper coloring using ℕ as the color type:
+  -- each edge has card 3, so we can extract two distinct vertices with distinct images.
+  have hprop : H.IsProperColoring φ := by
+    intro e he
+    -- Extract 3 distinct elements from e using H.uniform.
+    have hcard : e.card = 3 := H.uniform e he
+    -- Since e.card = 3 ≥ 2, there exist two distinct elements u ≠ v in e.
+    have hge : 1 < e.card := by omega
+    obtain ⟨u, hu, v, hv, huv⟩ := Finset.one_lt_card.mp hge
+    exact ⟨u, hu, v, hv, fun heq => huv (hφ heq)⟩
+  -- So χ(H) ≤ #ℕ = ℵ₀.
+  have hle : H.chromaticCardinal ≤ ℵ₀ := by
+    apply csInf_le
+    · -- The set {κ | ∃ C, #C = κ ∧ ∃ f, proper} is bounded below by 0.
+      exact ⟨0, fun _ ⟨_, _, _, _⟩ => Cardinal.zero_le _⟩
+    · exact ⟨ℕ, Cardinal.mk_nat, φ, hprop⟩
+  exact absurd (lt_of_lt_of_le hχ hle) (lt_irrefl _)
+
+/--
+**No hyperedges implies chromatic cardinal ≤ 1**: A 3-uniform hypergraph with no edges can
+be properly colored with a single color, so its chromatic cardinal is at most 1. In
+particular, $\chi(H) > \aleph_0$ implies `H` has at least one hyperedge.
+-/
+@[category undergraduate, AMS 5]
+theorem erdos_593.variants.nonempty_edges_if_large_chromatic
+    {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
+    H.edges.Nonempty := by
+  by_contra hempty
+  push_neg at hempty
+  -- H has no edges (hempty : H.edges = ∅), so any coloring is proper.
+  have hprop : H.IsProperColoring (fun _ : V => (0 : Fin 1)) := by
+    intro e he
+    rw [hempty] at he
+    exact (Set.mem_empty_iff_false e).mp he |>.elim
+  -- Hence χ(H) ≤ 1 < ℵ₀.
+  have hle : H.chromaticCardinal ≤ 1 := by
+    apply csInf_le
+    · exact ⟨0, fun _ ⟨_, _, _, _⟩ => Cardinal.zero_le _⟩
+    · refine ⟨Fin 1, ?_, fun _ => 0, hprop⟩
+      simp
+  have h1le : (1 : Cardinal) ≤ ℵ₀ := le_of_lt Cardinal.one_lt_aleph0
+  exact absurd (lt_of_lt_of_le hχ (hle.trans h1le)) (lt_irrefl _)
+
+/--
+**Monotonicity of the obligatory property**: If `F₁` appears in `F₂` and `F₂` is obligatory,
+then `F₁` is also obligatory.
+
+**Proof:** For any `H` with $\chi(H) > \aleph_0$, since `F₂` is obligatory, `F₂` appears
+in `H` via some injection `φ₂`. Since `F₁` appears in `F₂` via `φ₁`, the composition
+`φ₂ ∘ φ₁` witnesses that `F₁` appears in `H`.
+-/
+@[category undergraduate, AMS 5]
+theorem erdos_593.variants.obligatory_monotone
+    {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂]
+    {F₁ : ThreeUniformHypergraph W₁} {F₂ : ThreeUniformHypergraph W₂}
+    (h12 : F₁.Appears F₂) (hObl : IsObligatory F₂) :
+    IsObligatory F₁ := by
+  intro V _hV H hχ
+  obtain ⟨φ₂, hφ₂_inj, hφ₂_edge⟩ := hObl V H hχ
+  obtain ⟨φ₁, hφ₁_inj, hφ₁_edge⟩ := h12
+  refine ⟨φ₂ ∘ φ₁, hφ₂_inj.comp hφ₁_inj, fun e he => ?_⟩
+  -- e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ by Finset.image_image
+  -- (e.image φ₁).image φ₂ = e.image (φ₂ ∘ φ₁) by Finset.image_image
+  have heq : e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ := by
+    rw [Finset.image_image]
+  rw [heq]
+  exact hφ₂_edge _ (hφ₁_edge e he)
+
+/--
+**The empty hypergraph is trivially obligatory**: The 3-uniform hypergraph on `PEmpty` (no
+vertices, no edges) appears in every hypergraph via the empty injection.
+
+This degenerate case confirms the definition is well-formed.
+-/
+@[category undergraduate, AMS 5]
+theorem erdos_593.variants.empty_hypergraph_obligatory :
+    IsObligatory (W := PEmpty) ⟨∅, fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩ := by
+  intro V _hV H _hχ
+  exact ⟨IsEmpty.elim inferInstance, Function.injective_of_subsingleton _,
+    fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩
+
+end Erdos593

From 6565a7f2041ab2ba54dcf24d50e294e1a39a37fc Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Fri, 17 Apr 2026 13:51:03 +0100
Subject: [PATCH 2/7] Address review: move hypergraph infra to
 FormalConjecturesForMathlib, fix trivial statement
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Addresses review feedback by mo271:
- Move ThreeUniformHypergraph + related definitions to FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean
- Import them from new location in 593.lean
- Replace trivially-true main theorem with two substantive open conjectures:
  - erdos_593 (necessary condition): obligatory ⟹ 2-colorable
  - variants.two_colorable_implies_obligatory (converse, open)

Assisted by Claude (Anthropic).
---
 FormalConjectures/ErdosProblems/593.lean      |  95 ++++++----------
 FormalConjecturesForMathlib.lean              |   1 +
 .../Hypergraph/ThreeUniform.lean              | 105 ++++++++++++++++++
 3 files changed, 143 insertions(+), 58 deletions(-)
 create mode 100644 FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index 37e97b8210..00b072a295 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -15,6 +15,7 @@ limitations under the License.
 -/
 
 import FormalConjectures.Util.ProblemImports
+import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
 
 /-!
 # Erdős Problem 593
@@ -47,83 +48,62 @@ hypergraphs), the problem is completely solved:
 
 The 3-uniform case remains **open**.
 
-**Formalization notes:** We represent a 3-uniform hypergraph on vertex type `V` as a pair
-`(edges, uniform)` where `edges : Set (Finset V)` and every edge has cardinality 3. A proper
-coloring sends vertices to colors such that no hyperedge is monochromatic. The chromatic
-cardinal is the infimum of cardinalities of color types admitting a proper coloring. A finite
-hypergraph `F` *appears* in `H` if there is an injective vertex map carrying edges of `F`
-into edges of `H`.
+**Formalization notes:** See `FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform`
+for the definitions of `ThreeUniformHypergraph`, `IsProperColoring`, `chromaticCardinal`,
+`Appears`, and `IsObligatory` used throughout this file.
 
-We work at universe level `Type` (universe 0) throughout to avoid universe metavariable issues.
+Note: Mathlib does not yet have a general hypergraph API; the infrastructure in
+`FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform` fills that gap.
 -/
 
 open Cardinal Set SimpleGraph
 
 namespace Erdos593
 
-/- ## Definitions for 3-uniform hypergraphs -/
-
-/-- A **3-uniform hypergraph** on vertex type `V` is a set of 3-element `Finset`s.
-Each element of `edges` is a hyperedge, and `uniform` ensures each has exactly 3 vertices. -/
-structure ThreeUniformHypergraph (V : Type) where
-  /-- The set of hyperedges: each edge is a 3-element finset of vertices. -/
-  edges : Set (Finset V)
-  /-- Every hyperedge has exactly 3 vertices. -/
-  uniform : ∀ e ∈ edges, e.card = 3
-
-/-- A **proper coloring** of a 3-uniform hypergraph `H` by a color type `C` is a vertex
-coloring such that no hyperedge is monochromatic (all three vertices receive the same color). -/
-def ThreeUniformHypergraph.IsProperColoring {V : Type} (H : ThreeUniformHypergraph V)
-    {C : Type} (f : V → C) : Prop :=
-  ∀ e ∈ H.edges, ∃ u ∈ e, ∃ v ∈ e, f u ≠ f v
-
-/-- The **chromatic cardinal** of a 3-uniform hypergraph `H` is the infimum of cardinalities
-of color types admitting a proper coloring. We use `Cardinal.{0}` matching `Type`. -/
-noncomputable def ThreeUniformHypergraph.chromaticCardinal {V : Type}
-    (H : ThreeUniformHypergraph V) : Cardinal.{0} :=
-  sInf {κ : Cardinal.{0} | ∃ (C : Type), #C = κ ∧ ∃ f : V → C, H.IsProperColoring f}
-
-/-- A finite 3-uniform hypergraph `F` **appears** in `H` (as a sub-hypergraph) if there
-exists an injective vertex map `φ : W → V` that sends every hyperedge of `F` to a hyperedge
-of `H`. -/
-def ThreeUniformHypergraph.Appears {W V : Type} [DecidableEq V]
-    (F : ThreeUniformHypergraph W) (H : ThreeUniformHypergraph V) : Prop :=
-  ∃ φ : W → V, Function.Injective φ ∧
-    ∀ e ∈ F.edges, e.image φ ∈ H.edges
-
-/-- A finite 3-uniform hypergraph `F` on a `Fintype` vertex type is **obligatory** if it
-appears in every 3-uniform hypergraph (on a `Type`-valued vertex set) whose chromatic
-cardinal exceeds `ℵ₀`. -/
-def IsObligatory {W : Type} [Fintype W] (F : ThreeUniformHypergraph W) : Prop :=
-  ∀ (V : Type) [DecidableEq V] (H : ThreeUniformHypergraph V),
-    ℵ₀ < H.chromaticCardinal → F.Appears H
-
 /- ## Main open problem -/
 
 /--
-**Erdős Problem 593 ($500)**: Characterize those finite 3-uniform hypergraphs which appear in
-every 3-uniform hypergraph of chromatic number $> \aleph_0$.
+**Erdős Problem 593 ($500)**: Every obligatory finite 3-uniform hypergraph is 2-colorable.
 
 *Original statement (erdosproblems.com/593)*: "Characterize those finite 3-uniform hypergraphs
 which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$."
 
-**Background:** For graphs (2-uniform hypergraphs), the analogous problem is completely solved
-by Erdős, Galvin, and Hajnal [EGH75]: the obligatory finite graphs are precisely the finite
-bipartite graphs. No fixed odd cycle is obligatory. The 3-uniform case is open.
+**Background:** In the graph case ($r = 2$), Erdős, Galvin, and Hajnal [EGH75] proved that
+the obligatory finite graphs are exactly the finite bipartite graphs (= 2-colorable graphs).
+For the 3-uniform case, 2-colorability (Property B) is a natural necessary condition: if a
+finite 3-uniform hypergraph $F$ is not 2-colorable, one can construct a hypergraph with large
+chromatic number that contains no copy of $F$. Whether the converse holds (i.e., whether every
+2-colorable finite 3-uniform hypergraph is obligatory) is the main open question.
 
-**Formalization:** We express the problem as asking for a characterization predicate `P` for
-obligatory finite 3-uniform hypergraphs (formalized via `IsObligatory`). The `answer(sorry)`
-records that no such characterization is known.
+This theorem states the known necessary direction (every obligatory hypergraph is 2-colorable),
+which is the analogue of the graph case result. The full characterization remains open.
 
-**Prize:** \$500 (see erdosproblems.com/593).
+**Status:** OPEN (the necessary condition stated here is part of the open problem).
 
-**Status:** OPEN.
+**Prize:** \$500 (see erdosproblems.com/593).
 -/
 @[category research open, AMS 5]
 theorem erdos_593 : answer(sorry) ↔
-    ∃ (P : ∀ (W : Type) [Fintype W], ThreeUniformHypergraph W → Prop),
-      ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
-        IsObligatory F ↔ P W F := by
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      IsObligatory F → F.IsTwoColorable := by
+  sorry
+
+/--
+**Erdős Problem 593 — Converse direction (also open)**: Every finite 2-colorable 3-uniform
+hypergraph is obligatory.
+
+This is the converse of `erdos_593`: if the characterization of obligatory 3-uniform
+hypergraphs is exactly 2-colorability (as in the graph case), then every 2-colorable finite
+3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.
+
+**Status:** OPEN. The full Erdős Problem 593 is to determine whether `erdos_593` and
+`erdos_593.variants.two_colorable_implies_obligatory` both hold (i.e., whether
+`IsObligatory F ↔ F.IsTwoColorable`).
+-/
+@[category research open, AMS 5]
+theorem erdos_593.variants.two_colorable_implies_obligatory : answer(sorry) ↔
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      F.IsTwoColorable → IsObligatory F := by
   sorry
 
 /- ## Variants and partial results -/
@@ -243,7 +223,6 @@ theorem erdos_593.variants.obligatory_monotone
   obtain ⟨φ₁, hφ₁_inj, hφ₁_edge⟩ := h12
   refine ⟨φ₂ ∘ φ₁, hφ₂_inj.comp hφ₁_inj, fun e he => ?_⟩
   -- e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ by Finset.image_image
-  -- (e.image φ₁).image φ₂ = e.image (φ₂ ∘ φ₁) by Finset.image_image
   have heq : e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ := by
     rw [Finset.image_image]
   rw [heq]
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index c8e29b2edd..c2959020f3 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -36,6 +36,7 @@ public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
 public import FormalConjecturesForMathlib.Combinatorics.Additive.RestrictedSumset
 public import FormalConjecturesForMathlib.Combinatorics.Additive.VCDim
 public import FormalConjecturesForMathlib.Combinatorics.Basic
+public import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
 public import FormalConjecturesForMathlib.Combinatorics.LatinSquare
 public import FormalConjecturesForMathlib.Combinatorics.Ramsey
 public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim
diff --git a/FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean b/FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean
new file mode 100644
index 0000000000..8a247f7a4a
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean
@@ -0,0 +1,105 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Data.Finset.Card
+public import Mathlib.SetTheory.Cardinal.Basic
+public import Mathlib.SetTheory.Cardinal.Ordinal
+
+@[expose] public section
+
+/-!
+# 3-Uniform Hypergraphs
+
+This file defines the basic combinatorial infrastructure for 3-uniform hypergraphs used in
+formalizations of Erdős problems (e.g., Problem 593, Problem 1177).
+
+**Note:** Mathlib does not yet have a general hypergraph API. The definitions here fill that
+gap for the special case of 3-uniform hypergraphs (every edge has exactly 3 vertices).
+
+## Main definitions
+
+- `ThreeUniformHypergraph V` : a set of 3-element `Finset`s on a vertex type `V`
+- `ThreeUniformHypergraph.IsProperColoring` : vertex coloring with no monochromatic edge
+- `ThreeUniformHypergraph.chromaticCardinal` : minimum cardinality of a color type admitting
+  a proper coloring (a `Cardinal`-valued chromatic number, distinguishing infinite values)
+- `ThreeUniformHypergraph.Appears` : sub-hypergraph embedding (injective vertex map
+  carrying edges to edges)
+- `ThreeUniformHypergraph.IsTwoColorable` : vertex set has a 2-coloring with no monochromatic
+  edge (also called Property B); the 3-uniform analogue of bipartiteness for graphs
+- `IsObligatory` : a finite hypergraph appears in every hypergraph of chromatic cardinal > ℵ₀
+
+## References
+
+- Erdős, Galvin, Hajnal, *On set-systems having large chromatic number and not containing
+  prescribed subsystems*, Infinite and finite sets, 1975.
+-/
+
+open Cardinal Set
+
+/-- A **3-uniform hypergraph** on vertex type `V` is a set of 3-element `Finset`s.
+Each element of `edges` is a hyperedge, and `uniform` ensures each has exactly 3 vertices.
+
+Note: Mathlib does not yet have a general hypergraph API; this fills that gap for the
+3-uniform case relevant to Erdős problems 593 and 1177. -/
+structure ThreeUniformHypergraph (V : Type) where
+  /-- The set of hyperedges: each edge is a 3-element finset of vertices. -/
+  edges : Set (Finset V)
+  /-- Every hyperedge has exactly 3 vertices. -/
+  uniform : ∀ e ∈ edges, e.card = 3
+
+namespace ThreeUniformHypergraph
+
+/-- A **proper coloring** of a 3-uniform hypergraph `H` by a color type `C` is a vertex
+coloring such that no hyperedge is monochromatic (all three vertices receive the same color). -/
+def IsProperColoring {V : Type} (H : ThreeUniformHypergraph V) {C : Type} (f : V → C) : Prop :=
+  ∀ e ∈ H.edges, ∃ u ∈ e, ∃ v ∈ e, f u ≠ f v
+
+/-- The **chromatic cardinal** of a 3-uniform hypergraph `H` is the infimum of cardinalities
+of color types admitting a proper coloring.
+
+In contrast to a `ℕ∞`-valued chromatic number, this `Cardinal`-valued definition distinguishes
+between different infinite chromatic numbers (e.g., `ℵ₀` vs. `ℵ₁`). We work at `Type`
+(universe 0) throughout to avoid universe metavariable issues. -/
+noncomputable def chromaticCardinal {V : Type} (H : ThreeUniformHypergraph V) : Cardinal.{0} :=
+  sInf {κ : Cardinal.{0} | ∃ (C : Type), #C = κ ∧ ∃ f : V → C, H.IsProperColoring f}
+
+/-- A finite 3-uniform hypergraph `F` **appears** in `H` (as a sub-hypergraph) if there
+exists an injective vertex map `φ : W → V` that sends every hyperedge of `F` to a hyperedge
+of `H`. -/
+def Appears {W V : Type} [DecidableEq V] (F : ThreeUniformHypergraph W)
+    (H : ThreeUniformHypergraph V) : Prop :=
+  ∃ φ : W → V, Function.Injective φ ∧ ∀ e ∈ F.edges, e.image φ ∈ H.edges
+
+/-- A 3-uniform hypergraph `F` is **2-colorable** (has **Property B**) if there exists a
+2-coloring of its vertices with no monochromatic edge.
+
+This is the hypergraph analogue of bipartiteness for graphs: a graph is bipartite iff it
+is 2-colorable as a graph. For 3-uniform hypergraphs, 2-colorability is a necessary condition
+for being obligatory (every obligatory finite 3-uniform hypergraph is 2-colorable). -/
+def IsTwoColorable {V : Type} (F : ThreeUniformHypergraph V) : Prop :=
+  ∃ f : V → Fin 2, F.IsProperColoring f
+
+end ThreeUniformHypergraph
+
+/-- A finite 3-uniform hypergraph `F` on a `Fintype` vertex type is **obligatory** if it
+appears in every 3-uniform hypergraph (on a `Type`-valued vertex set) whose chromatic
+cardinal exceeds `ℵ₀`. -/
+def IsObligatory {W : Type} [Fintype W] (F : ThreeUniformHypergraph W) : Prop :=
+  ∀ (V : Type) [DecidableEq V] (H : ThreeUniformHypergraph V),
+    ℵ₀ < H.chromaticCardinal → F.Appears H
+
+end

From f6d7f8e2b8dc68eb4c2a84125941d5de080aeba4 Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Wed, 22 Apr 2026 14:42:53 +0100
Subject: [PATCH 3/7] docs: add verbatim source statement to module docstring

Mirrors the Round C docstring pass from the private repo's
phase1-infrastructure branch. Each Lean file now carries the
canonical source statement and upstream URL inline so reviewers
can verify formalization against the source without navigating
away from the diff.
---
 FormalConjectures/ErdosProblems/593.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index 00b072a295..afb5536ae1 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -20,6 +20,14 @@ import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
 /-!
 # Erdős Problem 593
 
+**Verbatim statement (Erdős #593, status O):**
+> Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number $>\aleph_0$.
+
+**Source:** https://www.erdosproblems.com/593
+
+**Notes:** OPEN - $500
+
+
 *Reference:* [erdosproblems.com/593](https://www.erdosproblems.com/593)
 
 *References for known results:*

From eb09c34a8b7f312acc6cf9eb6711007d4047002f Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Fri, 8 May 2026 01:47:24 +0100
Subject: [PATCH 4/7] fix(ErdosProblems/593): state main theorem as the
 conjectured iff (Paul-Lez review)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per Paul-Lez review on PR #3774, line 94: the source asks for a
characterization of the obligatory finite 3-uniform hypergraphs, not just
the necessary direction `IsObligatory F → F.IsTwoColorable`.

The natural conjectured characterization (analogous to Erdős–Galvin–Hajnal
for graphs: bipartite ⇔ obligatory) is

    IsObligatory F ↔ F.IsTwoColorable.

Rewrote the headline `erdos_593` as this iff, behind `answer(sorry)`. The
two directions are kept as separate `answer(sorry)`-d open variants:

  - obligatory_implies_two_colorable (necessary direction; new, replaces
    the previous one-direction headline)
  - two_colorable_implies_obligatory (sufficient direction; pre-existing)

Note: Paul-Lez's separate `category undergraduate` → `category textbook`
rename nit is deferred to a follow-up — the rename would require merging
upstream/main into this branch first to pull in the new CategoryLinter
keyword (the branch-local linter still expects `undergraduate`).

Builds cleanly:
    lake build FormalConjectures.ErdosProblems.«593»
---
 FormalConjectures/ErdosProblems/593.lean | 46 +++++++++++++++---------
 1 file changed, 30 insertions(+), 16 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index afb5536ae1..eeb21a7485 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -71,42 +71,56 @@ namespace Erdos593
 /- ## Main open problem -/
 
 /--
-**Erdős Problem 593 ($500)**: Every obligatory finite 3-uniform hypergraph is 2-colorable.
+**Erdős Problem 593 ($500)**: A finite 3-uniform hypergraph is obligatory iff it is
+2-colorable.
 
 *Original statement (erdosproblems.com/593)*: "Characterize those finite 3-uniform hypergraphs
 which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$."
 
 **Background:** In the graph case ($r = 2$), Erdős, Galvin, and Hajnal [EGH75] proved that
 the obligatory finite graphs are exactly the finite bipartite graphs (= 2-colorable graphs).
-For the 3-uniform case, 2-colorability (Property B) is a natural necessary condition: if a
-finite 3-uniform hypergraph $F$ is not 2-colorable, one can construct a hypergraph with large
-chromatic number that contains no copy of $F$. Whether the converse holds (i.e., whether every
-2-colorable finite 3-uniform hypergraph is obligatory) is the main open question.
+The natural conjectured 3-uniform analogue — and the conjectural characterization recorded
+here — is that obligatory finite 3-uniform hypergraphs are exactly the 2-colorable ones
+(Property B). The forward direction (`IsObligatory → IsTwoColorable`) and converse
+(`IsTwoColorable → IsObligatory`) are both open and stated as separate variants below.
 
-This theorem states the known necessary direction (every obligatory hypergraph is 2-colorable),
-which is the analogue of the graph case result. The full characterization remains open.
-
-**Status:** OPEN (the necessary condition stated here is part of the open problem).
+**Status:** OPEN.
 
 **Prize:** \$500 (see erdosproblems.com/593).
 -/
 @[category research open, AMS 5]
 theorem erdos_593 : answer(sorry) ↔
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      IsObligatory F ↔ F.IsTwoColorable := by
+  sorry
+
+/--
+**Erdős Problem 593 — Necessary direction (open)**: Every obligatory finite 3-uniform
+hypergraph is 2-colorable.
+
+This is the natural necessary condition for the conjectural characterization in `erdos_593`:
+if a finite 3-uniform hypergraph `F` is not 2-colorable, one expects to construct a
+hypergraph with large chromatic number that contains no copy of `F`.
+
+**Status:** OPEN.
+-/
+@[category research open, AMS 5]
+theorem erdos_593.variants.obligatory_implies_two_colorable : answer(sorry) ↔
     ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
       IsObligatory F → F.IsTwoColorable := by
   sorry
 
 /--
-**Erdős Problem 593 — Converse direction (also open)**: Every finite 2-colorable 3-uniform
+**Erdős Problem 593 — Sufficient direction (open)**: Every finite 2-colorable 3-uniform
 hypergraph is obligatory.
 
-This is the converse of `erdos_593`: if the characterization of obligatory 3-uniform
-hypergraphs is exactly 2-colorability (as in the graph case), then every 2-colorable finite
-3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.
+This is the converse direction of the `erdos_593` characterization: if 2-colorability
+matches the graph-case characterization (bipartite ⇔ obligatory), then every 2-colorable
+finite 3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number
+$> \aleph_0$.
 
-**Status:** OPEN. The full Erdős Problem 593 is to determine whether `erdos_593` and
-`erdos_593.variants.two_colorable_implies_obligatory` both hold (i.e., whether
-`IsObligatory F ↔ F.IsTwoColorable`).
+**Status:** OPEN. Together with `erdos_593.variants.obligatory_implies_two_colorable`,
+this implies `erdos_593`.
 -/
 @[category research open, AMS 5]
 theorem erdos_593.variants.two_colorable_implies_obligatory : answer(sorry) ↔

From a4e26480f8b4c51532580681424c480bb629229c Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Fri, 8 May 2026 13:52:45 +0100
Subject: [PATCH 5/7] =?UTF-8?q?fix(ErdosProblems/593):=20@[category=20unde?=
 =?UTF-8?q?rgraduate]=20=E2=86=92=20@[category=20textbook]=20+=20copyright?=
 =?UTF-8?q?=202026?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per Paul-Lez review on PR #3774. Mechanical nits applied on top of an
upstream/main merge to pick up the new attribute infrastructure (#3900).
---
 FormalConjectures/ErdosProblems/593.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index eeb21a7485..4cde464570 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -176,7 +176,7 @@ $> \aleph_0$ must have an uncountable vertex set.
 numbers as colors gives a proper coloring, so $\chi(H) \leq \#\mathbb{N} = \aleph_0$,
 contradicting $\chi(H) > \aleph_0$.
 -/
-@[category undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
     {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
     ¬ Countable V := by
@@ -206,7 +206,7 @@ theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
 be properly colored with a single color, so its chromatic cardinal is at most 1. In
 particular, $\chi(H) > \aleph_0$ implies `H` has at least one hyperedge.
 -/
-@[category undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_593.variants.nonempty_edges_if_large_chromatic
     {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
     H.edges.Nonempty := by
@@ -234,7 +234,7 @@ then `F₁` is also obligatory.
 in `H` via some injection `φ₂`. Since `F₁` appears in `F₂` via `φ₁`, the composition
 `φ₂ ∘ φ₁` witnesses that `F₁` appears in `H`.
 -/
-@[category undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_593.variants.obligatory_monotone
     {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂]
     {F₁ : ThreeUniformHypergraph W₁} {F₂ : ThreeUniformHypergraph W₂}
@@ -256,7 +256,7 @@ vertices, no edges) appears in every hypergraph via the empty injection.
 
 This degenerate case confirms the definition is well-formed.
 -/
-@[category undergraduate, AMS 5]
+@[category textbook, AMS 5]
 theorem erdos_593.variants.empty_hypergraph_obligatory :
     IsObligatory (W := PEmpty) ⟨∅, fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩ := by
   intro V _hV H _hχ

From 53f4f31628469323fce6630d5a0aeed85d1b4e12 Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Sun, 10 May 2026 18:21:43 +0100
Subject: [PATCH 6/7] fix(ErdosProblems/593): apply mo271 docstring conventions
 (review)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Collapse the two reference blocks into a single *References:* block
  in the module docstring; drop the duplicated verbatim statement,
  background paragraph, and formalization note.
- Trim the erdos_593 theorem docstring to the verbatim Erdős statement
  plus a single sentence about the conjectural characterization.
- Drop the **Status:** / **Prize:** mentions on erdos_593 and the
  three solved/open variants (already captured by @[category]).
- Add erdos_593.variants.implications_combine: the elementary Iff
  derivation showing that the two open implications jointly imply the
  characterization in erdos_593 (mo271 line-123 follow-up).

Follow-up flagged in mo271 line-147 review thread:
graph_case_bipartite_obligatory uses Nonempty (F →g G) (graph
homomorphism) but the hypergraph Appears definition uses an injective
vertex map. The two notions differ; switching to Nonempty (F ↪g G)
(graph embedding) is left as a follow-up. A docstring note records the
discrepancy so it isn't lost.
---
 FormalConjectures/ErdosProblems/593.lean | 90 ++++++++----------------
 1 file changed, 31 insertions(+), 59 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index 4cde464570..3199d3451c 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -20,48 +20,14 @@ import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
 /-!
 # Erdős Problem 593
 
-**Verbatim statement (Erdős #593, status O):**
-> Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number $>\aleph_0$.
-
-**Source:** https://www.erdosproblems.com/593
-
-**Notes:** OPEN - $500
-
-
-*Reference:* [erdosproblems.com/593](https://www.erdosproblems.com/593)
-
-*References for known results:*
+*References:*
+- [erdosproblems.com/593](https://www.erdosproblems.com/593)
 - [EGH75] Erdős, Paul and Galvin, Fred and Hajnal, András, On set-systems having large
   chromatic number and not containing prescribed subsystems.
   Infinite and finite sets (Colloq., Keszthely, 1973; dedicated to P. Erdős on his 60th
   birthday), Vol. I. Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 425–513.
 - [Er95d] Erdős, Paul, Some of my favourite problems in various branches of combinatorics.
   Matematiche (Catania) 47 (1992), no. 2, 231–240 (1995).
-
-**Problem (Erdős, $500)**: Characterize those finite 3-uniform hypergraphs which appear in
-every 3-uniform hypergraph of chromatic number $> \aleph_0$.
-
-**Background:** A hypergraph $H = (V, E)$ is **$r$-uniform** if every hyperedge $e \in E$
-has exactly $r$ vertices. The **chromatic number** $\chi(H)$ of a hypergraph is the minimum
-number of colors needed to color its vertices so that no hyperedge is monochromatic. A finite
-$r$-uniform hypergraph $F$ is **obligatory** (for the class of $r$-uniform hypergraphs with
-chromatic number $> \aleph_0$) if every $r$-uniform hypergraph with chromatic number
-$> \aleph_0$ contains a copy of $F$ as a sub-hypergraph.
-
-**Known (graph case, $r = 2$, Erdős–Galvin–Hajnal [EGH75]):** For graphs (2-uniform
-hypergraphs), the problem is completely solved:
-- A graph of chromatic number $\geq \aleph_1$ must contain all finite bipartite graphs.
-- No fixed odd cycle is obligatory: for every odd $k$, there exists a graph with chromatic
-  number $\aleph_1$ that contains no cycle of length $k$.
-
-The 3-uniform case remains **open**.
-
-**Formalization notes:** See `FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform`
-for the definitions of `ThreeUniformHypergraph`, `IsProperColoring`, `chromaticCardinal`,
-`Appears`, and `IsObligatory` used throughout this file.
-
-Note: Mathlib does not yet have a general hypergraph API; the infrastructure in
-`FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform` fills that gap.
 -/
 
 open Cardinal Set SimpleGraph
@@ -71,22 +37,14 @@ namespace Erdos593
 /- ## Main open problem -/
 
 /--
-**Erdős Problem 593 ($500)**: A finite 3-uniform hypergraph is obligatory iff it is
-2-colorable.
-
-*Original statement (erdosproblems.com/593)*: "Characterize those finite 3-uniform hypergraphs
-which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$."
-
-**Background:** In the graph case ($r = 2$), Erdős, Galvin, and Hajnal [EGH75] proved that
-the obligatory finite graphs are exactly the finite bipartite graphs (= 2-colorable graphs).
-The natural conjectured 3-uniform analogue — and the conjectural characterization recorded
-here — is that obligatory finite 3-uniform hypergraphs are exactly the 2-colorable ones
-(Property B). The forward direction (`IsObligatory → IsTwoColorable`) and converse
-(`IsTwoColorable → IsObligatory`) are both open and stated as separate variants below.
-
-**Status:** OPEN.
-
-**Prize:** \$500 (see erdosproblems.com/593).
+**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).
 -/
 @[category research open, AMS 5]
 theorem erdos_593 : answer(sorry) ↔
@@ -101,8 +59,6 @@ hypergraph is 2-colorable.
 This is the natural necessary condition for the conjectural characterization in `erdos_593`:
 if a finite 3-uniform hypergraph `F` is not 2-colorable, one expects to construct a
 hypergraph with large chromatic number that contains no copy of `F`.
-
-**Status:** OPEN.
 -/
 @[category research open, AMS 5]
 theorem erdos_593.variants.obligatory_implies_two_colorable : answer(sorry) ↔
@@ -119,8 +75,7 @@ matches the graph-case characterization (bipartite ⇔ obligatory), then every 2
 finite 3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number
 $> \aleph_0$.
 
-**Status:** OPEN. Together with `erdos_593.variants.obligatory_implies_two_colorable`,
-this implies `erdos_593`.
+Together with `erdos_593.variants.obligatory_implies_two_colorable`, this implies `erdos_593`.
 -/
 @[category research open, AMS 5]
 theorem erdos_593.variants.two_colorable_implies_obligatory : answer(sorry) ↔
@@ -128,6 +83,23 @@ theorem erdos_593.variants.two_colorable_implies_obligatory : answer(sorry) ↔
       F.IsTwoColorable → IsObligatory F := by
   sorry
 
+/--
+**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.
+-/
+@[category test, AMS 5]
+theorem erdos_593.variants.implications_combine
+    (h₁ : ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+            IsObligatory F → F.IsTwoColorable)
+    (h₂ : ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+            F.IsTwoColorable → IsObligatory F) :
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      IsObligatory F ↔ F.IsTwoColorable := by
+  intro W _ F
+  exact ⟨h₁ W F, h₂ W F⟩
+
 /- ## Variants and partial results -/
 
 /--
@@ -136,7 +108,9 @@ For the 2-uniform (graph) case, a graph of chromatic cardinal $> \aleph_0$ must
 finite bipartite graphs. Specifically, for every finite bipartite graph `F` and every graph
 `G` with chromatic cardinal $> \aleph_0$, there is a graph homomorphism from `F` to `G`.
 
-**Status:** SOLVED [EGH75].
+Note: this statement uses `Nonempty (F →g G)` (graph homomorphism), which is weaker than the
+injective vertex map used in the hypergraph `Appears` definition. A future revision may switch
+to `Nonempty (F ↪g G)` (graph embedding) to align with the hypergraph notion.
 -/
 @[category research solved, AMS 5]
 theorem erdos_593.variants.graph_case_bipartite_obligatory :
@@ -154,8 +128,6 @@ theorem erdos_593.variants.graph_case_bipartite_obligatory :
 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.
-
-**Status:** SOLVED [EGH75].
 -/
 @[category research solved, AMS 5]
 theorem erdos_593.variants.graph_case_no_odd_cycle :

From 7170485f2871a1c95439543d3226c4aca93ea961 Mon Sep 17 00:00:00 2001
From: Henryk Michalewski <henrykmichalewski@gmail.com>
Date: Tue, 12 May 2026 09:38:42 +0100
Subject: [PATCH 7/7] fix(ErdosProblems/593): switch
 graph_case_bipartite_obligatory to embedding (mo271 review); drop open/solved
 from docstrings

---
 FormalConjectures/ErdosProblems/593.lean | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/593.lean b/FormalConjectures/ErdosProblems/593.lean
index 3199d3451c..66050e7829 100644
--- a/FormalConjectures/ErdosProblems/593.lean
+++ b/FormalConjectures/ErdosProblems/593.lean
@@ -53,7 +53,7 @@ theorem erdos_593 : answer(sorry) ↔
   sorry
 
 /--
-**Erdős Problem 593 — Necessary direction (open)**: Every obligatory finite 3-uniform
+**Erdős Problem 593 — Necessary direction**: Every obligatory finite 3-uniform
 hypergraph is 2-colorable.
 
 This is the natural necessary condition for the conjectural characterization in `erdos_593`:
@@ -67,7 +67,7 @@ theorem erdos_593.variants.obligatory_implies_two_colorable : answer(sorry) ↔
   sorry
 
 /--
-**Erdős Problem 593 — Sufficient direction (open)**: Every finite 2-colorable 3-uniform
+**Erdős Problem 593 — Sufficient direction**: Every finite 2-colorable 3-uniform
 hypergraph is obligatory.
 
 This is the converse direction of the `erdos_593` characterization: if 2-colorability
@@ -103,14 +103,13 @@ theorem erdos_593.variants.implications_combine
 /- ## Variants and partial results -/
 
 /--
-**Graph analogue — bipartite graphs are obligatory (solved, Erdős–Galvin–Hajnal [EGH75])**:
+**Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75])**:
 For the 2-uniform (graph) case, a graph of chromatic cardinal $> \aleph_0$ must contain all
 finite bipartite graphs. Specifically, for every finite bipartite graph `F` and every graph
-`G` with chromatic cardinal $> \aleph_0$, there is a graph homomorphism from `F` to `G`.
+`G` with chromatic cardinal $> \aleph_0$, there is a graph embedding from `F` into `G`.
 
-Note: this statement uses `Nonempty (F →g G)` (graph homomorphism), which is weaker than the
-injective vertex map used in the hypergraph `Appears` definition. A future revision may switch
-to `Nonempty (F ↪g G)` (graph embedding) to align with the hypergraph notion.
+This uses `Nonempty (F ↪g G)` (graph embedding), aligned with the injective vertex map
+used in the hypergraph `Appears` definition.
 -/
 @[category research solved, AMS 5]
 theorem erdos_593.variants.graph_case_bipartite_obligatory :
@@ -118,13 +117,13 @@ theorem erdos_593.variants.graph_case_bipartite_obligatory :
     ∀ (V : Type*) (G : SimpleGraph V),
       ℵ₀ < G.chromaticCardinal →
       ∀ (W : Type*) [Fintype W] (F : SimpleGraph W), F.IsBipartite →
-        Nonempty (F →g G) := by
+        Nonempty (F ↪g G) := by
   simp only [true_iff]
   -- This is the Erdős–Galvin–Hajnal theorem [EGH75].
   sorry
 
 /--
-**Graph analogue — no odd cycle is obligatory (solved, Erdős–Galvin–Hajnal [EGH75])**:
+**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.