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 statement3 of 3

Graham claims this is "easy to see".

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

1¬Erdos189.Erdos189For2    (fun a b c d =>3      (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧4        (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧5          (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction ∧ dist a b = dist b c)6    fun a b c d => dist a b * dist b c

SolvedStatement only, no proof

Sources

Search problems.science