Erdős problem 1128
Erdős Problem 1128 (disproved by Prikry–Mills, 1978):
Sources
FormalConjectures/ErdosProblems/
1128.lean
Retained formal statement
Prikry–Mills counterexample (key lemma):
There exists a 2-colouring of a set of cardinality cubed such that no countable box is monochromatic.
This is the unpublished result of Prikry and Mills (1978). The proof proceeds by transfinite induction along , which has uncountable cofinality, ensuring every countable box is non-monochromatic.
∃ X, ∃ (_ : Cardinal.mk X = Cardinal.aleph 1), ∃ f, ∀ (A₁ B₁ C₁ : Set X), Cardinal.mk ↑A₁ = Cardinal.aleph 0 → Cardinal.mk ↑B₁ = Cardinal.aleph 0 → Cardinal.mk ↑C₁ = Cardinal.aleph 0 → ¬Erdos1128.IsMonochromaticBox f A₁ B₁ C₁SolvedStatement only, no proof