Erdős Problem 189

Reference: erdosproblems.com/189

def Erdos189For (P : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop) (A : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ) : Prop

Erdős problem 189 asked whether the below holds for all rectangles.

Equations

• One or more equations did not get rendered due to their size.

theorem erdos_189 : (Erdos189For (fun (a b c d : EuclideanSpace ℝ (Fin 2)) => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction) fun (a b c d : EuclideanSpace ℝ (Fin 2)) => dist a b * dist b c) ↔ False

If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area?

Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.)

Solved (with answer False, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero).

theorem erdos_189.variants.square : ¬Erdos189For (fun (a b c d : EuclideanSpace ℝ (Fin 2)) => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ dist a b = dist b c) fun (a b c d : EuclideanSpace ℝ (Fin 2)) => dist a b * dist b c

Graham claims this is "easy to see".

theorem erdos_189.variants.parallelogram : ¬Erdos189For (fun (a b c d : EuclideanSpace ℝ (Fin 2)) => (affineSpan ℝ {a, b}).Parallel (affineSpan ℝ {c, d}) ∧ (affineSpan ℝ {a, d}).Parallel (affineSpan ℝ {b, c})) fun (a b c d : EuclideanSpace ℝ (Fin 2)) => dist a b * dist b c * (EuclideanGeometry.oangle a b c).sin

Seems to be open, as of January 2025.