/-
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 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).
[EHR73] Erdős, Paul and Hajnal, András and Rothschild, Bruce, On chromatic number of graphs and set-systems. Cambridge Summer School in Mathematical Logic (Cambridge, 1971), Lecture Notes in Math. 337, Springer (1973), 531–538.
@[expose] public sectionopen 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$.
The answer is the set of obligatory finite 3-uniform hypergraphs, represented here on the
labelled vertex sets Fin n.
Two-colorability (Property B) is a necessary condition, see
erdos_593.variants.obligatory_implies_two_colorable, but it is not sufficient: two triples
sharing a pair form a 2-colorable hypergraph that is not obligatory, see
erdos_593.variants.common_pair_not_obligatory. In the graph case ($r = 2$) the problem is
completely solved by Erdős–Galvin–Hajnal [EGH75]: the obligatory graphs are exactly the finite
bipartite graphs.
A resolution has been claimed by E. Li (arXiv:2606.24882, 2026); at the time of writing erdosproblems.com still lists the problem as open.
@[category research open, AMS 5]
theorem erdos_593 :
{p : Σ n : ℕ, ThreeUniformHypergraph (Fin n) | IsObligatory p.2} = answer(sorry) := ⊢ {p | IsObligatory p.snd} = sorry
All goals completed! 🐙Necessary direction: every obligatory finite 3-uniform hypergraph is 2-colorable.
This follows from two constructions in [EGH75]. By [EHR73] (see [EGH75, p. 426]) there are
3-uniform hypergraphs of arbitrarily large chromatic number consisting of edge-disjoint
triples, so an obligatory F is linear (no two edges share two vertices). By the remark
preceding [EGH75, Theorem 10.9] there are, for every infinite cardinal $\kappa$, 3-uniform
hypergraphs of chromatic number $> \kappa$ all of whose linear sub-hypergraphs are
2-colorable. An obligatory F appears in such a hypergraph, hence is 2-colorable.
@[category research solved, AMS 5]
theorem erdos_593.variants.obligatory_implies_two_colorable : answer(True) ↔
∀ (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! 🐙Sufficient direction fails: it is not the case that every finite 2-colorable 3-uniform hypergraph is obligatory.
The hypergraph commonPair with edges ${0,1,2}$ and ${0,1,3}$ is 2-colorable but does
not appear in the 3-uniform hypergraphs of large chromatic number consisting of edge-disjoint
triples constructed in [EHR73], see erdos_593.variants.common_pair_not_obligatory.
@[category research solved, AMS 5]
theorem erdos_593.variants.two_colorable_implies_obligatory : answer(False) ↔
∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
F.IsTwoColorable → IsObligatory F := ⊢ False ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F
All goals completed! 🐙The 3-uniform hypergraph on four vertices consisting of two triples sharing a pair, ${0,1,2}$ and ${0,1,3}$.
def commonPair : ThreeUniformHypergraph (Fin 4) :=
ThreeUniformHypergraph.ofFinset {{0, 1, 2}, {0, 1, 3}} (⊢ {{0, 1, 2}, {0, 1, 3}}.IsThreeUniform ⊢ ∀ e ∈ {{0, 1, 2}, {0, 1, 3}}, e.card = 3; All goals completed! 🐙)Two triples sharing a pair are 2-colorable: color the shared pair with one color and the remaining two vertices with the other.
@[category test, AMS 5]
theorem erdos_593.variants.commonPair_isTwoColorable : commonPair.IsTwoColorable :=
⟨fun i => if i.val < 2 then 0 else 1, ⊢ commonPair.IsProperColoring fun i ↦ if ↑i < 2 then 0 else 1
e:Finset (Fin 4)he:e ∈ commonPair.edges⊢ ∃ u ∈ e, ∃ v ∈ e, (fun i ↦ if ↑i < 2 then 0 else 1) u ≠ (fun i ↦ if ↑i < 2 then 0 else 1) v
e:Finset (Fin 4)he:e ∈ {{0, 1, 2}, {0, 1, 3}}⊢ ∃ u ∈ e, ∃ v ∈ e, (fun i ↦ if ↑i < 2 then 0 else 1) u ≠ (fun i ↦ if ↑i < 2 then 0 else 1) v
⊢ ∀ e ∈ {{0, 1, 2}, {0, 1, 3}},
∃ u ∈ e, ∃ v ∈ e, (fun i ↦ if ↑i < 2 then 0 else 1) u ≠ (fun i ↦ if ↑i < 2 then 0 else 1) v
All goals completed! 🐙⟩
Two triples sharing a pair are not obligatory: by [EHR73] (see [EGH75, p. 426]) there are
3-uniform hypergraphs of arbitrarily large chromatic number consisting of edge-disjoint
triples, and commonPair does not appear in any of them.
@[category research solved, AMS 5]
theorem erdos_593.variants.common_pair_not_obligatory : ¬ IsObligatory commonPair := ⊢ ¬IsObligatory commonPair
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 F ⊑ G (SimpleGraph.IsContained, an injective graph homomorphism), aligned with
the injective edge-preserving map used in the hypergraph Appears definition. A graph embedding
F ↪g G would require an induced copy, which the theorem does not provide.
@[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 →
F ⊑ G := ⊢ True ↔
∀ (V : Type u_1) (G : SimpleGraph V),
ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → F ⊑ G
⊢ ∀ (V : Type u_1) (G : SimpleGraph V),
ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → F ⊑ 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