Erdős Problem 189

Reference: erdosproblems.com/189

def Erdos189.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 Erdos189.erdos_189 : False ↔ 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 ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun (a b c d : EuclideanSpace ℝ (Fin 2)) => dist a b * dist b c

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).

This was formalized in Lean by Alexeev and Kovac using Aristotle.

theorem Erdos189.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 ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).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 Erdos189.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.