Skip to content

Erdős problem 189

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/189.lean

Formal Conjectures

FormalConjectures/ErdosProblems/189.leanErdos189.erdos_1897 linesExact file
False ↔  Erdos189.Erdos189For    (fun a b c d =>      (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 => 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:189
  • PLBY Lean proofsErdosProblems.Erdos189

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page