1167.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

9 declarations, 5 contain sorry, 0 declared as axioms

Erdő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). Without $\kappa_\alpha > r$ it is also false: with $r = 2$, $\lambda = \aleph_0$ and targets $(2, \aleph_1)$, the premise $2^{\aleph_0} \to (3, \aleph_1)^3$ holds, but a constant colouring of the pairs of $\aleph_0$ has neither a red pair nor a blue set of size $\aleph_1$.

Imports (1)

FormalConjecturesUtil

theorem Erdos1167.erdos_1167 Erdős Problem 1167 sorry line 55 source
Source documentation
Erdős Problem 1167. Let $r \geq 2$ be finite, $\gamma \geq 2$, and $\lambda$ be an infinite cardinal. Let $\kappa_\alpha > r$ 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.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal, Ordinal.ToType, LT.lt, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1167 : answer(sorry) ↔
    ∀ (r : ℕ), 2 ≤ r →
    ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam →
    ∀ (γ : Ordinal.{u}), 2 ≤ γ →
    ∀ (κ : γ.ToType → Cardinal.{u}), (∀ α, (r : Cardinal.{u}) < κ α) →
      cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) →
      cardinalPartitionRel lam r γ κ := by
…
```
theorem Erdos1167.erdos_1167.variants.finite_targets Finite-target case sorry line 71 source
Source documentation
Finite-target case. When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$ is the ordinary natural-number successor. Special case of erdos_1167.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal, Ordinal.ToType, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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})) := by
…
```
theorem Erdos1167.erdos_1167.variants.binary_colors Binary-color case sorry line 82 source
Source documentation
Binary-color case. The $\gamma = 2$ specialization (two color classes).

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal.ToType, Ordinal, LT.lt, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (κ : (2 : Ordinal.{u}).ToType → Cardinal.{u}) (hκ : ∀ α, (r : Cardinal.{u}) < κ α) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) 2 (fun α => κ α + 1) →
    cardinalPartitionRel lam r 2 κ := by
…
```
theorem Erdos1167.erdos_1167.variants.infinite_targets Infinite-target case sorry line 99 source
Source documentation
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).

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal, Ordinal.ToType, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 γ κ := by
…
```
theorem Erdos1167.erdos_1167.variants.r_eq_two $r = 2$ case sorry line 113 source
Source documentation
$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.

depends on sorry what this means
Statement uses: Cardinal, LE.le, Cardinal.aleph0, Ordinal, OfNat.ofNat, Nat, Ordinal.ToType, LT.lt, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem r_eq_two (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u})
    (hκ : ∀ α, (2 : Cardinal.{u}) < κ α) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) 3 γ (fun α => κ α + 1) →
    cardinalPartitionRel lam 2 γ κ := by
…
```
def Erdos1167.i0 A canonical element of the type (1 : Ordinal).ToType line 130 source
Source documentation
A canonical element of the type (1 : Ordinal).ToType.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ordinal.ToType, OfNat.ofNat, Ordinal
Proof uses: Inhabited.default
6 instances, coercions and auxiliary constants left out.
```
noncomputable def i0 : (1 : Ordinal.{u}).ToType := default
…
```
lemma Erdos1167.cardinalPartitionRel_one The partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$ line 136 source
Source documentation
The partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Cardinal, Nat, Ordinal.ToType, OfNat.ofNat, Ordinal, Iff, Combinatorics.cardinalPartitionRel, GE.ge, Erdos1167.i0
Proof uses: id, Iff.intro, Eq, Cardinal.mk, Subtype, Finset, Finset.card, Exists, Set, And, LE.le, Subtype.mk, Quotient.out, Cardinal.mk_out, Subsingleton.elim, Cardinal.mk_set_le, Eq.mp, congrArg, Eq.symm, Eq.mpr and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma cardinalPartitionRel_one (μ : Cardinal.{u}) (r : ℕ)
    (ν : (1 : Ordinal.{u}).ToType → Cardinal.{u}) :
    cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν i0 := by
…
```
Mentions: Erdos1167.i0
theorem Erdos1167.erdos_1167.unrestricted_is_false The unrestricted version of Erdős Problem 1167 (without the condition $\gamma \geq 2$ from the original Erdős–Hajnal list) is false line 163 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal, Ordinal.ToType, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: OrderEmbedding, Cardinal.aleph, le_refl, Eq.mpr, GE.ge, id, Eq, congrArg, propext, Erdos1167.cardinalPartitionRel_one, Cardinal.add_one_of_aleph0_le, Cardinal.aleph0_le_aleph, Cardinal.aleph_one_le_continuum, LT.lt, Cardinal.aleph0_lt_aleph_one, And.right, Eq.mp
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1167.unrestricted_is_false :
    ¬ (∀ (r : ℕ), 2 ≤ r →
    ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam →
    ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}),
      cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) →
      cardinalPartitionRel lam r γ κ) := by
…
```
theorem Erdos1167.erdos_1167.variants.infinite_targets_needs_bound The infinite_targets variant without the bound $\kappa_\alpha \leq \lambda$ is false line 187 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Nat, LE.le, OfNat.ofNat, Cardinal, Cardinal.aleph0, Ordinal, Ordinal.ToType, Combinatorics.cardinalPartitionRel, HPow.hPow, HAdd.hAdd
Proof uses: le_refl, LT.lt.le, Cardinal.cantor, Eq.mpr, GE.ge, id, Eq, congrArg, propext, Erdos1167.cardinalPartitionRel_one, And.right, Eq.mp
27 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1167.variants.infinite_targets_needs_bound :
    ¬ (∀ (r : ℕ), 2 ≤ r →
    ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam →
    ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ i, ℵ₀ ≤ κ i) →
      cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ →
      cardinalPartitionRel lam r γ κ) := by
…
```