Erdős problem 189

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

189.lean

Retained formal statement1 of 3

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.

FormalConjectures/ErdosProblems/189.leanErdos189.erdos_1897 linesExact file

1False ↔2  Erdos189.Erdos189For3    (fun a b c d =>4      (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧5        (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧6          (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction)7    fun a b c d => dist a b * dist b c

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.