Skip to content

Erdős problem 1128

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1128.lean

Retained formal statement1 of 4

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

Erdős asked whether every 2-colouring of A×B×CA \times B \times C, where ∣A∣=∣B∣=∣C∣=ℵ1|A| = |B| = |C| = \aleph_1, must contain a monochromatic countable box A1×B1×C1A_1 \times B_1 \times C_1 with ∣A1∣=∣B1∣=∣C1∣=ℵ0|A_1| = |B_1| = |C_1| = \aleph_0.

The answer is No: Prikry and Mills constructed a 2-colouring of ω13\omega_1^3 with no monochromatic countable box.

Note: The positive statement asserts that every 2-colouring of every ℵ13\aleph_1^3 contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.

FormalConjectures/ErdosProblems/1128.leanErdos1128.erdos_112810 linesExact file
False ↔  ∀ (A B C : Type),    Cardinal.mk A = Cardinal.aleph 1 →      Cardinal.mk B = Cardinal.aleph 1 →        Cardinal.mk C = Cardinal.aleph 1 →          ∀ (f : A → B → C → Fin 2),            ∃ A₁ B₁ C₁,              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