/-
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 FormalConjecturesUtilErdős Problem 593
References:
[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 SimpleGraphnamespace Erdos593Erdő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 := ⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable
All goals completed! 🐙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 := ⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorable
All goals completed! 🐙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 := ⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F
All goals completed! 🐙
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 := h₁:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorableh₂:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F⊢ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable
h₁:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorableh₂:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory FW:Typeinst✝:Fintype WF:ThreeUniformHypergraph W⊢ IsObligatory F ↔ F.IsTwoColorable
All goals completed! 🐙
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) := ⊢ True ↔
∀ (V : Type u_1) (G : SimpleGraph V),
ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)
⊢ ∀ (V : Type u_1) (G : SimpleGraph V),
ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)
-- This is the Erdős–Galvin–Hajnal theorem [EGH75].
All goals completed! 🐙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) := ⊢ True ↔ ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ V G, G.chromaticCardinal = ℵ_ 1 ∧ IsEmpty (cycleGraph k →g G)
⊢ ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ V G, G.chromaticCardinal = ℵ_ 1 ∧ IsEmpty (cycleGraph k →g G)
-- This is the Erdős–Galvin–Hajnal theorem [EGH75].
All goals completed! 🐙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$.
V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φ⊢ False
-- So χ(H) ≤ #ℕ = ℵ₀.
V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φhle:H.chromaticCardinal ≤ ℵ₀⊢ False
All goals completed! 🐙
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.
V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x ↦ 0hle:H.chromaticCardinal ≤ 1⊢ False
V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x ↦ 0hle:H.chromaticCardinal ≤ 1h1le:1 ≤ ℵ₀⊢ False
All goals completed! 🐙
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.
W₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalφ₂:W₂ → Vhφ₂_inj:Function.Injective φ₂hφ₂_edge:∀ e ∈ F₂.edges, Finset.image φ₂ e ∈ H.edgesφ₁:W₁ → W₂hφ₁_inj:Function.Injective φ₁hφ₁_edge:∀ e ∈ F₁.edges, Finset.image φ₁ e ∈ F₂.edgese:Finset W₁he:e ∈ F₁.edgesheq:Finset.image (φ₂ ∘ φ₁) e = Finset.image φ₂ (Finset.image φ₁ e)⊢ Finset.image φ₂ (Finset.image φ₁ e) ∈ H.edges
All goals completed! 🐙
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⟩ := ⊢ IsObligatory { edges := ∅, uniform := ⋯ }
V:Type_hV:DecidableEq VH:ThreeUniformHypergraph V_hχ:ℵ₀ < H.chromaticCardinal⊢ { edges := ∅, uniform := ⋯ }.Appears H
All goals completed! 🐙end Erdos593