/-
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 1128
Reference: erdosproblems.com/1128
open Cardinal Set Ordinal Ordernamespace Erdos1128A 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$.
def IsMonochromaticBox {A B C : Type*} (f : A → B → C → Fin 2)
(A₁ : Set A) (B₁ : Set B) (C₁ : Set C) : Prop :=
∃ c : Fin 2, ∀ a ∈ A₁, ∀ b ∈ B₁, ∀ c' ∈ C₁, f a b c' = c
The set of countable ordinals, expressed using Mathlib's ω_ 1.
private abbrev Omega1 := {o : Ordinal.{0} // o < ω_ 1}The set of ordinals strictly below any $\gamma < \omega_1$ is countable.
@[category API, AMS 5]
private lemma countable_Iio_of_lt_omega1 {γ : Ordinal} (hγ : γ < ω_ 1) :
(Set.Iio γ).Countable := γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ (Iio γ).Countable
rwa [γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ #↑(Iio γ) ≤ ℵ₀ γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ Cardinal.lift.{u_1 + 1, u_1} γ.card ≤ ℵ₀ γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ γ.card ≤ ℵ₀
γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ γ.card < ℵ_ 1 γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ γ < ω_ 1γ:Ordinal.{u_1}hγ:γ < ω_ 1⊢ γ < ω_ 1set_option backward.isDefEq.respectTransparency false in
Initial segments of ω₁ (as sets of Omega1 elements) are countable.
This is the subtype-order version of countable_Iio_of_lt_omega1.
@[category API, AMS 5]
private lemma countable_Iio_omega1 (γ : Omega1) : (Set.Iio γ : Set Omega1).Countable := γ:Omega1⊢ (Iio γ).Countable
-- The injection a ↦ ⟨a.1.val, a.2⟩ sends ↑(Iio γ : Set Omega1) into ↑(Iio γ.val : Set Ord)
-- and the codomain is countable by countable_Iio_of_lt_omega1.
γ:Omega1hcount:Countable ↑(Iio ↑γ)⊢ (Iio γ).Countable
-- Goal: (Set.Iio γ : Set Omega1).Countable = Set.Countable (Set.Iio γ)
-- = Countable ↥(Set.Iio γ : Set Omega1) (by definition of Set.Countable)
γ:Omega1hcount:Countable ↑(Iio ↑γ)⊢ Countable ↑(Iio γ)
-- Use Function.Injective.countable with the injection a ↦ ⟨a.1.val, a.2⟩.
γ:Omega1hcount:Countable ↑(Iio ↑γ)⊢ Function.Injective fun a ↦ ⟨↑↑a, ⋯⟩
-- `h` arrives as an unreduced application of the injection.
γ:Omega1hcount:Countable ↑(Iio ↑γ)av:Ordinal.{0}hav_ω₁:av < ω_ 1hav_γ:⟨av, hav_ω₁⟩ ∈ Iio γbv:Ordinal.{0}hbv_ω₁:bv < ω_ 1hbv_γ:⟨bv, hbv_ω₁⟩ ∈ Iio γh:(fun a ↦ ⟨↑↑a, ⋯⟩) ⟨⟨av, hav_ω₁⟩, hav_γ⟩ = (fun a ↦ ⟨↑↑a, ⋯⟩) ⟨⟨bv, hbv_ω₁⟩, hbv_γ⟩⊢ ⟨⟨av, hav_ω₁⟩, hav_γ⟩ = ⟨⟨bv, hbv_ω₁⟩, hbv_γ⟩
γ:Omega1hcount:Countable ↑(Iio ↑γ)av:Ordinal.{0}hav_ω₁:av < ω_ 1hav_γ:⟨av, hav_ω₁⟩ ∈ Iio γbv:Ordinal.{0}hbv_ω₁:bv < ω_ 1hbv_γ:⟨bv, hbv_ω₁⟩ ∈ Iio γh:av = bv⊢ ⟨⟨av, hav_ω₁⟩, hav_γ⟩ = ⟨⟨bv, hbv_ω₁⟩, hbv_γ⟩
All goals completed! 🐙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).
S:Set Omega1hS:S.Countablehemp:S = ∅⊢ ∃ γ, ∀ s ∈ ∅, s < γ
All goals completed! 🐙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.
@[category research solved, AMS 3 5]
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₁ := ⊢ ∃ X,
∃ (_ : #X = ℵ_ 1), ∃ f, ∀ (A₁ B₁ C₁ : Set X), #↑A₁ = ℵ_ 0 → #↑B₁ = ℵ_ 0 → #↑C₁ = ℵ_ 0 → ¬IsMonochromaticBox f A₁ B₁ C₁
-- The Prikry–Mills construction (1978, unpublished):
-- Take X = ω_ 1.ToType, which has cardinality ℵ₁ (by mk_ord_toType).
--
-- Construction by transfinite induction on γ < ω₁:
-- * For each γ, since Iio γ is countable (card_le_aleph0_of_lt_omega1), choose an
-- injection e_γ : Iio γ → ℕ. The injection is chosen to "kill" all countable
-- boxes (A_ξ × B_ξ × C_ξ)_{ξ<γ} that are relevant to stage γ.
-- * Define f(α, β, γ) = 0 if e_γ(α) < e_γ(β) when both α, β ∈ Iio γ; else f = 1.
-- (Extend arbitrarily when the coordinates don't satisfy α, β < γ.)
--
-- Non-monochromaticity proof sketch:
-- Given a putative monochromatic box A₁ × B₁ × C₁ (say with color 0), the
-- diagonalization at the stage γ* = min(C₁ above sup(A₁ ∪ B₁)) ensures that
-- e_{γ*} was specifically chosen so that the coloring is NOT constant on A₁ × B₁
-- via γ*. The key counting argument:
-- * sup(A₁ ∪ B₁) < ω₁ (by countable_subset_bdd, since A₁ ∪ B₁ is countable).
-- * At stage γ*, the image e_{γ*}(A₁) ⊆ ℕ and e_{γ*}(B₁) ⊆ ℕ are both
-- infinite, so neither "∀ a < all b" nor "∀ a > all b" can hold.
-- * This gives a witness pair (α, β) where f(α, β, γ*) ≠ color 0.
--
-- The full formalization requires transfinite inductive choice (choosing e_γ for
-- each γ via Well.rec or Ordinal.limitRecOn) and a careful stage counting argument
-- using ω₁'s uncountable cofinality.
All goals completed! 🐙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.
@[category research solved, AMS 3 5]
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₁ := ⊢ False ↔
∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁
-- `answer(False)` reduces to `False` in the default elaborator mode.
-- The goal is: False ↔ ∀ A B C, |A| = ℵ₁ → |B| = ℵ₁ → |C| = ℵ₁ →
-- ∀ f, ∃ monochromatic countable box.
-- (→): False implies anything.
-- (←): The Prikry–Mills theorem provides A B C of size ℵ₁ and a 2-colouring
-- with no monochromatic countable box, contradicting the hypothesis.
⊢ False →
∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁⊢ (∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2),
∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁) →
False
⊢ False →
∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁ h:False⊢ ∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁; All goals completed! 🐙
⊢ (∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2),
∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁) →
False h:∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁⊢ False
-- Obtain the Prikry–Mills counterexample: a type X of cardinality ℵ₁ with a
-- 2-colouring f : X → X → X → Fin 2 having no monochromatic countable box.
h:∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁X:TypehX:#X = ℵ_ 1f:X → X → X → Fin 2hf:∀ (A₁ B₁ C₁ : Set X), #↑A₁ = ℵ_ 0 → #↑B₁ = ℵ_ 0 → #↑C₁ = ℵ_ 0 → ¬IsMonochromaticBox f A₁ B₁ C₁⊢ False
-- Apply h to X (playing the roles of A, B, C), using |X| = ℵ₁.
h:∀ (A B C : Type),
#A = ℵ_ 1 →
#B = ℵ_ 1 →
#C = ℵ_ 1 →
∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, #↑A₁ = ℵ_ 0 ∧ #↑B₁ = ℵ_ 0 ∧ #↑C₁ = ℵ_ 0 ∧ IsMonochromaticBox f A₁ B₁ C₁X:TypehX:#X = ℵ_ 1f:X → X → X → Fin 2hf:∀ (A₁ B₁ C₁ : Set X), #↑A₁ = ℵ_ 0 → #↑B₁ = ℵ_ 0 → #↑C₁ = ℵ_ 0 → ¬IsMonochromaticBox f A₁ B₁ C₁A₁:Set XB₁:Set XC₁:Set XhA:#↑A₁ = ℵ_ 0hB:#↑B₁ = ℵ_ 0hC:#↑C₁ = ℵ_ 0hbox:IsMonochromaticBox f A₁ B₁ C₁⊢ False
-- The Prikry–Mills theorem says no countably infinite box is monochromatic.
-- Since #A₁ = aleph 0, #B₁ = aleph 0, #C₁ = aleph 0, this is a contradiction.
All goals completed! 🐙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$.
@[category research solved, AMS 3 5]
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₁ := ⊢ ∃ f,
∀ (A₁ : Set { o // o < ω_ 1 }) (B₁ : Set { o // o < ω_ 1 }) (C₁ : Set { o // o < ω_ 1 }),
#↑A₁ = ℵ_ 0 → #↑B₁ = ℵ_ 0 → #↑C₁ = ℵ_ 0 → ¬IsMonochromaticBox f A₁ B₁ C₁
-- This is the explicit form of the Prikry–Mills theorem on
-- ω₁ = {o : Ordinal // o < ω_ 1}.
--
-- Key ingredients (all proved in the auxiliary lemmas above):
-- 1. countable_Iio_of_lt_omega1: For each γ < ω₁, the set Iio γ is countable.
-- 2. countable_subset_bdd: Any countable A₁ ⊆ ω₁ is bounded below ω₁.
-- (Uses iSup_sequence_lt_omega_one and the regularity of ω₁.)
--
-- Construction: By transfinite induction, choose injections e_γ : Iio γ → ℕ
-- (possible by countable_Iio_of_lt_omega1 and Countable.exists_injective_nat)
-- to "kill" every countable box. The coloring is:
-- f(α, β, γ) = 0 if e_γ(α) < e_γ(β) (when α, β < γ)
-- f(α, β, γ) = 1 otherwise
--
-- Non-monochromaticity: For any countable A₁, B₁, C₁ ⊆ ω₁, by
-- countable_subset_bdd there exists γ ∈ C₁ above sup(A₁ ∪ B₁). At this γ,
-- e_γ embeds A₁ ∪ B₁ injectively into ℕ, giving infinite disjoint images.
-- Two infinite subsets of ℕ cannot have all elements of one strictly less than
-- all elements of the other, giving a contradiction with monochromaticity.
--
-- Universe note: {o : Ordinal // o < ω_ 1} lives in Type 1 while the
-- abstract prikryMills uses X : Type 0. The construction here is self-contained
-- and does not need to be reduced to prikryMills.
All goals completed! 🐙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.
A₁:Set Omega1B₁:Set Omega1hA_unc:¬A₁.CountablehB_unc:¬B₁.CountableA₁_unbdd:∀ (γ : Omega1), ∃ a ∈ A₁, γ ≤ aB₁_unbdd:∀ (γ : Omega1), ∃ b ∈ B₁, γ ≤ bhB_ne:B₁.Nonemptyhcol:∀ a ∈ A₁, ∀ b ∈ B₁, (if ↑a < ↑b then 0 else 1) = (fun i ↦ i) ⟨1, ⋯⟩a₀:Omega1ha₀:a₀ ∈ A₁ha₀_succ_lt:↑a₀ + 1 < ω_ 1b':Omega1hb'B:b' ∈ B₁hb'_ge:⟨↑a₀ + 1, ha₀_succ_lt⟩ ≤ b'hlt:↑a₀ < ↑b'hcol_val:¬↑a₀ < ↑b'⊢ False
All goals completed! 🐙end Erdos1128