1128.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, 2 contain sorry, 0 declared as axioms

Erdős Problem 1128

Reference: erdosproblems.com/1128

Imports (1)

FormalConjecturesUtil

def Erdos1128.IsMonochromaticBox Documented declaration: IsMonochromaticBox line 35 source
Source documentation
A subset $A_1 \times B_1 \times C_1$ of $A \times B \times C$ is monochromatic under a 2-colouring $f : A \to B \to C \to \operatorname{Fin} 2$ if $f$ is constant on $A_1 \times B_1 \times C_1$.

no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Set
Proof uses: Exists, Membership.mem, Eq
3 instances, coercions and auxiliary constants left out.
```
def IsMonochromaticBox {A B C : Type*} (f : A → B → C → Fin 2)
    (A₁ : Set A) (B₁ : Set B) (C₁ : Set C) : Prop :=
…
```
abbrev Erdos1128.Omega1 The set of countable ordinals, expressed using Mathlib's ω_ 1 line 45 source
Source documentation
The set of countable ordinals, expressed using Mathlib's ω_ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Subtype, Ordinal, LT.lt, OrderEmbedding, Ordinal.omega, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
abbrev Omega1 := {o : Ordinal.{0} // o < ω_ 1}
…
```
lemma Erdos1128.countable_Iio_of_lt_omega1 The set of ordinals strictly below any $\gamma < \omega_1$ is countable line 49 source
Source documentation
The set of ordinals strictly below any $\gamma < \omega_1$ is countable.
```
private lemma countable_Iio_of_lt_omega1 {γ : Ordinal} (hγ : γ < ω_ 1) :
    (Set.Iio γ).Countable := by
…
```
lemma Erdos1128.countable_Iio_omega1 Initial segments of ω₁ (as sets of Omega1 elements) are countable line 58 source
Source documentation
Initial segments of ω₁ (as sets of Omega1 elements) are countable. This is the subtype-order version of countable_Iio_of_lt_omega1.
```
private lemma countable_Iio_omega1 (γ : Omega1) : (Set.Iio γ : Set Omega1).Countable := by
…
```
Mentions: Erdos1128.Omega1
lemma Erdos1128.countable_subset_bdd Any countable subset of $\omega_1$ is bounded strictly below some element of $\omega_1$ line 76 source
Source documentation
Any countable subset of $\omega_1$ is bounded strictly below some element of $\omega_1$. This uses the key property that $\omega_1$ has uncountable cofinality (it is regular).
```
private lemma countable_subset_bdd (S : Set Omega1) (hS : S.Countable) :
    ∃ γ : Omega1, ∀ s ∈ S, s < γ := by
…
```
Mentions: Erdos1128.Omega1
theorem Erdos1128.erdos_1128.prikryMills Prikry–Mills counterexample (key lemma): There exists a 2-colouring sorry line 106 source
Source documentation
Prikry–Mills counterexample (key lemma):
There exists a 2-colouring $f$ of a set of cardinality $\aleph_1$ cubed such that no countable box $A_1 \times B_1 \times C_1$ is monochromatic.
This is the unpublished result of Prikry and Mills (1978). The proof proceeds by transfinite induction along $\omega_1$, which has uncountable cofinality, ensuring every countable box is non-monochromatic.

depends on sorry what this means
Statement uses: Exists, Eq, Cardinal, Cardinal.mk, OrderEmbedding, Ordinal, Cardinal.aleph, OfNat.ofNat, Fin, Nat, Set, Not, Erdos1128.IsMonochromaticBox
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1128.prikryMills :
    ∃ (X : Type) (_ : #X = aleph 1) (f : X → X → X → Fin 2),
      ∀ (A₁ B₁ C₁ : Set X),
        #A₁ = aleph 0 → #B₁ = aleph 0 → #C₁ = aleph 0 →
        ¬ IsMonochromaticBox f A₁ B₁ C₁ := by
…
```
Mentions: Erdos1128.IsMonochromaticBox
theorem Erdos1128.erdos_1128 Documented declaration: erdos_1128 line 151 source
Source documentation
Erdős Problem 1128 (disproved by Prikry–Mills, 1978):
Erdős asked whether every 2-colouring of $A \times B \times C$, where $|A| = |B| = |C| = \aleph_1$, must contain a monochromatic countable box $A_1 \times B_1 \times C_1$ with $|A_1| = |B_1| = |C_1| = \aleph_0$.
The answer is No: Prikry and Mills constructed a 2-colouring of $\omega_1^3$ with no monochromatic countable box.
Note: The positive statement asserts that every 2-colouring of every $\aleph_1^3$ contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.

depends on sorry what this means
Statement uses: Iff, False, Eq, Cardinal, Cardinal.mk, OrderEmbedding, Ordinal, Cardinal.aleph, OfNat.ofNat, Fin, Nat, Exists, Set, And, Erdos1128.IsMonochromaticBox
Proof uses: Iff.intro, False.elim, Not, Erdos1128.erdos_1128.prikryMills
26 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1128 : answer(False) ↔
    ∀ (A B C : Type) (_ : #A = aleph 1) (_ : #B = aleph 1) (_ : #C = aleph 1)
      (f : A → B → C → Fin 2),
      ∃ (A₁ : Set A) (B₁ : Set B) (C₁ : Set C),
        #A₁ = aleph 0 ∧ #B₁ = aleph 0 ∧ #C₁ = aleph 0 ∧
        IsMonochromaticBox f A₁ B₁ C₁ := by
…
```
Mentions: Erdos1128.IsMonochromaticBox
theorem Erdos1128.erdos_1128.variants.prikryMills_explicit Documented declaration: prikryMills_explicit sorry line 187 source
Source documentation
Explicit form of Prikry–Mills:
There exists a 2-colouring of $\omega_1 \times \omega_1 \times \omega_1$ such that for every countably infinite $A_1, B_1, C_1 \subseteq \omega_1$, the box $A_1 \times B_1 \times C_1$ is not monochromatic.
This is the content of the Prikry–Mills theorem (1978, unpublished), stated using Lean's ordinal type {o : Ordinal // o < ω_ 1} as the representation of $\omega_1$.

depends on sorry what this means
Statement uses: Exists, Subtype, Ordinal, LT.lt, OrderEmbedding, Ordinal.omega, OfNat.ofNat, Fin, Nat, Set, Eq, Cardinal, Cardinal.mk, Cardinal.aleph, Not, Erdos1128.IsMonochromaticBox
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1128.variants.prikryMills_explicit :
    ∃ (f : {o : Ordinal // o < ω_ 1} →
           {o : Ordinal // o < ω_ 1} →
           {o : Ordinal // o < ω_ 1} → Fin 2),
      ∀ (A₁ B₁ C₁ : Set {o : Ordinal // o < ω_ 1}),
        #A₁ = aleph 0 → #B₁ = aleph 0 → #C₁ = aleph 0 →
        ¬ IsMonochromaticBox f A₁ B₁ C₁ := by
…
```
Mentions: Erdos1128.IsMonochromaticBox
theorem Erdos1128.erdos_1128.variants.two_dimensional_false The claim that every 2-colouring of $\omega_1 \times \omega_1$ has an uncountable monochromatic product rectangle is false in ZFC line 236 source
Source documentation
The claim that every 2-colouring of $\omega_1 \times \omega_1$ has an uncountable monochromatic product rectangle is false in ZFC.
Counterexample: The ordering colouring $f(\alpha, \beta) = 0$ iff $\alpha < \beta$ has no uncountable monochromatic product rectangle $A_1 \times B_1$.
Proof: If $A_1 \times B_1$ were monochromatic with colour 0, then every element of $A_1$ would be strictly less than every element of $B_1$, making $A_1$ bounded above in $\omega_1$; but any bounded subset of $\omega_1$ is countable (since initial segments are countable), contradicting $A_1$ being uncountable. The colour-1 case is symmetric with the roles of $A_1$ and $B_1$ swapped.
Note: The correct classical result for 2-colourings of pairs (not products) is the Erdős–Rado theorem $\omega_1 \to (\omega_1)^2_2$, which concerns unordered pairs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Erdos1128.Omega1, Fin, OfNat.ofNat, Nat, Exists, Set, And, Set.Countable, Membership.mem, Eq
Proof uses: ite, LT.lt, Ordinal, OrderEmbedding, Ordinal.omega, False, LE.le, Classical.byContradiction, Set.Countable.mono, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Set.Nonempty, Eq.rec, EmptyCollection.emptyCollection, Set.countable_empty and 49 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1128.variants.two_dimensional_false :
    ¬ ∀ (f : Omega1 → Omega1 → Fin 2),
        ∃ (A₁ B₁ : Set Omega1),
          ¬ A₁.Countable ∧ ¬ B₁.Countable ∧
          ∃ c : Fin 2, ∀ a ∈ A₁, ∀ b ∈ B₁, f a b = c := by
…
```
Mentions: Erdos1128.Omega1, c