/-
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 1167
Reference: erdosproblems.com/1167
The original Erdős–Hajnal problem list gives the additional conditions $\gamma \geq 2$, $r < \omega$,
and $\kappa_\alpha > r$. Without $\gamma \geq 2$, the statement is false: taking $\gamma = 1$ and
$\kappa_0 = \aleph_1$ with $\lambda = \aleph_0$ gives a counterexample, since the partition relation
with one color degenerates to a cardinality comparison (see erdos_1167.unrestricted_is_false).
open Cardinal Ordinal Combinatoricsnamespace Erdos1167universe uErdős Problem 1167. Let $r \geq 2$ be finite, $\gamma \geq 2$, and $\lambda$ be an infinite cardinal. Let $\kappa_\alpha$ be cardinals for all $\alpha < \gamma$. Is it true that $$2^\lambda \to (\kappa_\alpha + 1){\alpha < \gamma}^{r+1}$$ implies $$\lambda \to (\kappa\alpha){\alpha < \gamma}^r?$$ Here $+$ means cardinal addition, so that $\kappa\alpha + 1 = \kappa_\alpha$ if $\kappa_\alpha$ is infinite.
A problem of Erdős, Hajnal, and Rado.
@[category research open, AMS 5]
theorem erdos_1167 : answer(sorry) ↔
∀ (r : ℕ), 2 ≤ r →
∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam →
∀ (γ : Ordinal.{u}), 2 ≤ γ →
∀ (κ : γ.ToType → Cardinal.{u}),
cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) →
cardinalPartitionRel lam r γ κ := ⊢ True ↔
∀ (r : ℕ),
2 ≤ r →
∀ (lam : Cardinal.{u}),
ℵ₀ ≤ lam →
∀ (γ : Ordinal.{u}),
2 ≤ γ →
∀ (κ : γ.ToType → Cardinal.{u}),
(cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κ
All goals completed! 🐙namespace erdos_1167.variants
Finite-target case. When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$
is the ordinary natural-number successor. Special case of erdos_1167.
@[category research open, AMS 5]
theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
(γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) :
cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ
(fun α => (n α : Cardinal.{u}) + 1) →
cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u})) := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γn:γ.ToType → ℕ⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ ↑(n α) + 1) → cardinalPartitionRel lam r γ fun α ↦ ↑(n α)
All goals completed! 🐙Binary-color case. The $\gamma = 2$ specialization (two color classes).
@[category research open, AMS 5]
theorem binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
(κ : (2 : Ordinal.{u}).ToType → Cardinal.{u}) :
cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) 2 (fun α => κ α + 1) →
cardinalPartitionRel lam r 2 κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamκ:ToType 2 → Cardinal.{u}⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) 2 fun α ↦ κ α + 1) → cardinalPartitionRel lam r 2 κ
All goals completed! 🐙
Infinite-target case. When all $\kappa_\alpha \geq \aleph_0$ are infinite and bounded by
$\lambda$, $\kappa_\alpha + 1 = \kappa_\alpha$, so the hypothesis simplifies to a "pure"
stepping-down lemma:
$$2^\lambda \to (\kappa_\alpha){\alpha<\gamma}^{r+1} \implies
\lambda \to (\kappa\alpha){\alpha<\gamma}^r.$$
The condition $\kappa\alpha \leq \lambda$ is needed to avoid a size obstruction: without it, the
conclusion would require a subset of $\lambda$ of size $\kappa_\alpha > \lambda$, which is impossible
(see infinite_targets_needs_bound).
@[category research open, AMS 5]
theorem infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
(γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ i, ℵ₀ ≤ κ i)
(hκ_le : ∀ i, κ i ≤ lam) :
cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ →
cardinalPartitionRel lam r γ κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}hκ:∀ (i : γ.ToType), ℵ₀ ≤ κ ihκ_le:∀ (i : γ.ToType), κ i ≤ lam⊢ cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ
All goals completed! 🐙$r = 2$ case. The stepping-down from 3-uniform to 2-uniform partition relations: $2^\lambda \to (\kappa_\alpha + 1){\alpha<\gamma}^3$ implies $\lambda \to (\kappa\alpha)_{\alpha<\gamma}^2$. Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.
@[category research open, AMS 5]
theorem r_eq_two (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
(γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) :
cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) 3 γ (fun α => κ α + 1) →
cardinalPartitionRel lam 2 γ κ := lam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}⊢ (cardinalPartitionRel (2 ^ lam) 3 γ fun α ↦ κ α + 1) → cardinalPartitionRel lam 2 γ κ
All goals completed! 🐙end erdos_1167.variants
A canonical element of the type (1 : Ordinal).ToType.
noncomputable def i0 : (1 : Ordinal.{u}).ToType := defaultThe partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$.
μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i
μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i
μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0⊢ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i0
μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0s:Finset Ahs:s.card = rhsH:↑s ⊆ H⊢ col ⟨s, hs⟩ = i0
All goals completed! 🐙The unrestricted version of Erdős Problem 1167 (without the condition $\gamma \geq 2$ from the original Erdős–Hajnal list) is false. Taking $\gamma = 1$, $\kappa_0 = \aleph_1$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (\aleph_1 + 1)^3_1$ holds since $2^{\aleph_0} \geq \aleph_1$, but the conclusion $\aleph_0 \to (\aleph_1)^2_1$ fails since $\aleph_0 < \aleph_1$.
h:∀ (r : ℕ),
2 ≤ r →
∀ (lam : Cardinal.{u}),
ℵ₀ ≤ lam →
∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}),
(cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α ↦ ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ ℵ_ 1 + 1h3:ℵ₀ ≥ ℵ_ 1⊢ False
h:∀ (r : ℕ),
2 ≤ r →
∀ (lam : Cardinal.{u}),
ℵ₀ ≤ lam →
∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}),
(cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α ↦ ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ ℵ_ 1 + 1h3:ℵ₀ ≥ ℵ_ 1h4:ℵ₀ < ℵ_ 1⊢ False
All goals completed! 🐙
The infinite_targets variant without the bound $\kappa_\alpha \leq \lambda$ is false.
Taking $\gamma = 1$, $\kappa_0 = 2^{\aleph_0}$, $\lambda = \aleph_0$: the premise
$2^{\aleph_0} \to (2^{\aleph_0})^3_1$ holds since $2^{\aleph_0} \leq 2^{\aleph_0}$, but the
conclusion $\aleph_0 \to (2^{\aleph_0})^2_1$ fails by Cantor's theorem.
h:∀ (r : ℕ),
2 ≤ r →
∀ (lam : Cardinal.{u}),
ℵ₀ ≤ lam →
∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}),
(∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun x ↦ 2 ^ ℵ₀) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ 2 ^ ℵ₀h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ 2 ^ ℵ₀h3:ℵ₀ ≥ 2 ^ ℵ₀⊢ False
All goals completed! 🐙end Erdos1167