593.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

12 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 593

References:

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).
[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.

Imports (1)

FormalConjecturesUtil

theorem Erdos593.erdos_593 Erdős Problem 593 ($500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$ sorry line 62 source
Source documentation
Erdő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.

depends on sorry what this means
Statement uses: Eq, Set, Sigma, Nat, UniformHypergraph, Fin, OfNat.ofNat, Set.ofPred, UniformHypergraph.IsObligatory, Sigma.fst, Sigma.snd, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593 :
    {p : Σ n : ℕ, UniformHypergraph (Fin n) 3 | p.2.IsObligatory} = answer(sorry) := by
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.obligatory_implies_two_colorable Necessary direction: every obligatory finite 3-uniform hypergraph is 2-colorable sorry line 77 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, Fintype, UniformHypergraph, OfNat.ofNat, Nat, UniformHypergraph.IsObligatory, UniformHypergraph.IsNColorable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.obligatory_implies_two_colorable : answer(True) ↔
    ∀ (W : Type) [Fintype W] (F : UniformHypergraph W 3),
      F.IsObligatory → F.IsNColorable 2 := by
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.two_colorable_implies_obligatory Sufficient direction fails: it is not the case that every finite 2-colorable 3-uniform hypergraph is obligatory sorry line 91 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, False, Fintype, UniformHypergraph, OfNat.ofNat, Nat, UniformHypergraph.IsNColorable, UniformHypergraph.IsObligatory
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.two_colorable_implies_obligatory : answer(False) ↔
    ∀ (W : Type) [Fintype W] (F : UniformHypergraph W 3),
      F.IsNColorable 2 → F.IsObligatory := by
…
```
Mentions: UniformHypergraph
def Erdos593.commonPair The 3-uniform hypergraph on four vertices consisting of two triples sharing a pair, $\{0,1,2\}$ and $\{0,1,3\}$ line 98 source
Source documentation
The 3-uniform hypergraph on four vertices consisting of two triples sharing a pair, $\{0,1,2\}$ and $\{0,1,3\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UniformHypergraph, Fin, OfNat.ofNat, Nat
Proof uses: UniformHypergraph.ofFinset, Insert.insert, Finset, Singleton.singleton
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def commonPair : UniformHypergraph (Fin 4) 3 :=
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.commonPair_isTwoColorable Two triples sharing a pair are 2-colorable: color the shared pair with one color and the remaining two vertices with the other line 104 source
Source documentation
Two triples sharing a pair are 2-colorable: color the shared pair with one color and the remaining two vertices with the other.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UniformHypergraph.IsNColorable, OfNat.ofNat, Nat, Fin, Erdos593.commonPair
Proof uses: Exists.intro, Hypergraph.IsProperColoring, UniformHypergraph.toHypergraph, ite, LT.lt, Iff.mpr, UniformHypergraph.IsProperColoring, UniformHypergraph.ofFinset, Insert.insert, Finset, Singleton.singleton, id, Finset.IsUniform, of_decide_eq_true, Membership.mem, Eq, Finset.card, Bool, Decidable.decide, Bool.true and 6 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.commonPair_isTwoColorable : commonPair.IsNColorable 2 :=
…
```
theorem Erdos593.erdos_593.variants.common_pair_not_obligatory Two triples sharing a pair are not obligatory: by [EHR73] (see [EGH75, p sorry line 116 source
Source documentation
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.

depends on sorry what this means
Statement uses: Not, UniformHypergraph.IsObligatory, OfNat.ofNat, Nat, Fin, Erdos593.commonPair
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.common_pair_not_obligatory : ¬ commonPair.IsObligatory := by
…
```
theorem Erdos593.erdos_593.variants.graph_case_bipartite_obligatory Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75]): For the 2-uniform (graph) case, a graph of chromatic cardinal sorry line 132 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, SimpleGraph, LT.lt, Cardinal, Cardinal.aleph0, SimpleGraph.chromaticCardinal, Fintype, SimpleGraph.IsBipartite, SimpleGraph.IsContained
Proof uses: Eq.mpr, id, Eq, true_iff, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem Erdos593.erdos_593.variants.graph_case_no_odd_cycle Graph analogue — no odd cycle is obligatory (Erdős–Galvin–Hajnal [EGH75]): For every odd sorry line 149 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, Nat, Odd, LE.le, OfNat.ofNat, Exists, SimpleGraph, And, Eq, Cardinal, SimpleGraph.chromaticCardinal, OrderEmbedding, Ordinal, Cardinal.aleph, IsEmpty, SimpleGraph.Hom, Fin, SimpleGraph.cycleGraph
Proof uses: Eq.mpr, id, true_iff, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
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
…
```
theorem Erdos593.erdos_593.variants.uncountable_vertices_if_large_chromatic Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal $> \aleph_0$ must have an uncountable vertex set line 168 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UniformHypergraph, OfNat.ofNat, Nat, LT.lt, Cardinal, Cardinal.aleph0, UniformHypergraph.chromaticCardinal, Not, Countable
Proof uses: Function.Injective, Exists, False, Countable.exists_injective_nat, UniformHypergraph.IsProperColoring, UniformHypergraph.isProperColoring_of_injective, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mp, Cardinal.mk, congrArg, Cardinal.mk_eq_aleph0, UniformHypergraph.chromaticCardinal_le, absurd and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
    {V : Type} (H : UniformHypergraph V 3) (hχ : ℵ₀ < H.chromaticCardinal) :
    ¬ Countable V := by
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.nonempty_edges_if_large_chromatic 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 line 185 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UniformHypergraph, OfNat.ofNat, Nat, LT.lt, Cardinal, Cardinal.aleph0, UniformHypergraph.chromaticCardinal, Set.Nonempty, Set, Hypergraph.edgeSet, UniformHypergraph.toHypergraph
Proof uses: Classical.byContradiction, Not, UniformHypergraph.IsProperColoring, Fin, Membership.mem, False.elim, Exists, And, Ne, Iff.mp, EmptyCollection.emptyCollection, False, Set.mem_empty_iff_false, Eq.mp, congrArg, Eq, LE.le, Cardinal.mk, Eq.trans, Fintype.card and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.nonempty_edges_if_large_chromatic
    {V : Type} (H : UniformHypergraph V 3) (hχ : ℵ₀ < H.chromaticCardinal) :
    H.edgeSet.Nonempty := by
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.obligatory_monotone Monotonicity of the obligatory property: If F₁ appears in F₂ and F₂ is obligatory, then F₁ is also obligatory line 209 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, UniformHypergraph, OfNat.ofNat, Nat, UniformHypergraph.Appears, UniformHypergraph.IsObligatory
Proof uses: LT.lt, Cardinal, Cardinal.aleph0, UniformHypergraph.chromaticCardinal, UniformHypergraph.Appears.trans
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.obligatory_monotone
    {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂]
    {F₁ : UniformHypergraph W₁ 3} {F₂ : UniformHypergraph W₂ 3}
    (h12 : F₁.Appears F₂) (hObl : F₂.IsObligatory) :
    F₁.IsObligatory := by
…
```
Mentions: UniformHypergraph
theorem Erdos593.erdos_593.variants.empty_hypergraph_obligatory The empty hypergraph is trivially obligatory: The 3-uniform hypergraph on PEmpty (no vertices, no edges) appears in every hypergraph via the empty injection line 224 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UniformHypergraph.IsObligatory, OfNat.ofNat, Nat, PEmpty, UniformHypergraph.ofFinset, EmptyCollection.emptyCollection, Finset
Proof uses: DecidableEq, UniformHypergraph, LT.lt, Cardinal, Cardinal.aleph0, UniformHypergraph.chromaticCardinal, Exists.intro, And, Function.Injective, LE.le, Set, Hypergraph.edgeSet, Hypergraph.image, UniformHypergraph.toHypergraph, IsEmpty.elim, inferInstance, IsEmpty, And.intro, Function.injective_of_subsingleton, of_eq_true and 26 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_593.variants.empty_hypergraph_obligatory :
    UniformHypergraph.IsObligatory (W := PEmpty) (k := 3)
…
```
Mentions: UniformHypergraph.IsObligatory