Skip to content

Erdős problem 1128

Erdős Problem 1128 (disproved by Prikry–Mills, 1978):

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1128.lean

Retained formal statement2 of 4

Prikry–Mills counterexample (key lemma):

There exists a 2-colouring ff of a set of cardinality 1\aleph_1 cubed such that no countable box A1×B1×C1A_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 ω1\omega_1, which has uncountable cofinality, ensuring every countable box is non-monochromatic.

FormalConjectures/ErdosProblems/1128.leanErdos1128.erdos_1128.prikryMills7 linesExact file
X,  ∃ (_ : Cardinal.mk X = Cardinal.aleph 1),f,      ∀ (ABC₁ : Set X),        Cardinal.mkA₁ = Cardinal.aleph 0 →          Cardinal.mkB₁ = Cardinal.aleph 0 →            Cardinal.mkC₁ = Cardinal.aleph 0 → ¬Erdos1128.IsMonochromaticBox f ABC
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page