Erdős problem 189 · problems.science

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

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

189.lean

Retained formal statement2 of 3

Seems to be open, as of January 2025.

FormalConjectures/ErdosProblems/189.leanErdos189.erdos_189.variants.parallelogram4 linesExact file

1¬Erdos189.Erdos189For2    (fun a b c d =>3      (affineSpan ℝ {a, b}).Parallel (affineSpan ℝ {c, d}) ∧ (affineSpan ℝ {a, d}).Parallel (affineSpan ℝ {b, c}))4    fun a b c d => dist a b * dist b c * (EuclideanGeometry.oangle a b c).sin

OpenStatement only, no proof

Sources

Search problems.science