Add Erdős Problem 593 (obligatory 3-uniform subhypergraphs, $500 prize) by henrykmichalewski · Pull Request #3774 · google-deepmind/formal-conjectures

henrykmichalewski · 2026-04-16T12:23:38Z

fixes #813

Problem

Erdős Problem 593: https://www.erdosproblems.com/593 ($500 prize)

Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number > ℵ₀.

…s ($500 prize) 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).

henrykmichalewski · 2026-04-17T08:23:38Z

Closes #813

mo271

Thanks!
There are some problems here, see comments, I only reviewed up to the first trivially provable open (or not so open) statement

mo271 · 2026-04-17T09:11:55Z

+
+**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.


All this stuff here should go to where it belongs, for instance the Formalisation notes on 3-uniform hypergraphs closer to where the hypergraphs are defined

mo271 · 2026-04-17T09:13:18Z

+/- ## 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


Those definitions should go in our FormalConjecturesForMathlib dir in an appropriate place. I'm surprised that Mathlib doesn't have hypergraphs already

mo271 · 2026-04-17T09:16:17Z

+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


AS stated this is trivially true:

theorem erdos_593 : answer(True) ↔ ∃ (P : ∀ (W : Type) [Fintype W], ThreeUniformHypergraph W → Prop), ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ P W F := by exact ⟨fun _ => ⟨fun _ _ F => IsObligatory F, fun _ _ _ => Iff.rfl⟩, fun _ => trivial⟩

The original problem asks to characterize which finite 3-uniform hypergraphs are obligatory i.e., to give a structural description in terms of simpler properties (analogous to "bipartite" in the graph case). Bare existential quantification over predicates cannot capture this: in formal logic, every property trivially characterizes itself.

This is a known difficulty with formalizing "characterize X" problems. Potentially our answer(sorry) mechanism can help here?

… fix trivial statement Per mo271's review feedback on PR google-deepmind#3774 (Problem 593, $500 prize): 1. Refactor: move ThreeUniformHypergraph, IsProperColoring, chromaticCardinal, Appears, IsTwoColorable, and IsObligatory out of the problem file into FormalConjecturesForMathlib/Combinatorics/Hypergraph/ThreeUniform.lean and register it in FormalConjecturesForMathlib.lean. 2. Fix the trivially-true main theorem: the old statement '∃ P, ∀ F, IsObligatory F ↔ P W F' was proved by the reviewer with a one-liner (P := IsObligatory). Replace with two non-trivial open conjectures based on the 2-colorability (Property B) characterization: - erdos_593: every obligatory finite 3-uniform hypergraph is 2-colorable - erdos_593.variants.two_colorable_implies_obligatory: the converse These mirror the graph case (EGH75: obligatory graphs = bipartite graphs). Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>

… fix trivial statement 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).

github-actions bot added the erdos-problems Erdős Problems label Apr 16, 2026

mo271 reviewed Apr 17, 2026

View reviewed changes

henrykmichalewski force-pushed the add-problem-593 branch from 49b3486 to 6565a7f Compare April 19, 2026 09:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Add Erdős Problem 593 (obligatory 3-uniform subhypergraphs, $500 prize)#3774
henrykmichalewski wants to merge 2 commits intogoogle-deepmind:mainfrom
henrykmichalewski:add-problem-593

henrykmichalewski commented Apr 16, 2026 •

edited by mo271

Loading

Uh oh!

henrykmichalewski commented Apr 17, 2026

Uh oh!

mo271 left a comment

Uh oh!

mo271 Apr 17, 2026

Uh oh!

mo271 Apr 17, 2026

Uh oh!

mo271 Apr 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

henrykmichalewski commented Apr 16, 2026 • edited by mo271 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Contents

Uh oh!

henrykmichalewski commented Apr 17, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

mo271 Apr 17, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 Apr 17, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 Apr 17, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

henrykmichalewski commented Apr 16, 2026 •

edited by mo271

Loading