Add Erdős Problem 593 (obligatory 3-uniform subhypergraphs, $500 prize)

FormalConjectures/ErdosProblems/593.lean

@@ -0,0 +1,237 @@
+/-
+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
+import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
+
+/-!
+# Erdős Problem 593
+
+*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).
+-/
+
+open Cardinal Set SimpleGraph
+
+namespace Erdos593
+
+/- ## 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$.
+
+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) ↔
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      IsObligatory F ↔ F.IsTwoColorable := by
+  sorry
+
+/--
+**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`:
+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`.
+-/
+@[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 — Sufficient direction**: Every finite 2-colorable 3-uniform
+hypergraph is obligatory.
+
+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$.
+
+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) ↔
+    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
+      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 -/
+
+/--
+**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 embedding from `F` into `G`.
+
+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 :
+    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 (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.
+-/
+@[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 textbook, 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 textbook, 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 textbook, 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
+  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 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χ
+  exact ⟨IsEmpty.elim inferInstance, Function.injective_of_subsingleton _,
+    fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩
+
+end Erdos593

FormalConjecturesForMathlib.lean

@@ -37,6 +37,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

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