Skip to content

Erdős problem 1090

Let k3k\geq 3. Does there exist a finite set AR2A\subset \mathbb{R}^2 such that, in any 22-colouring of AA, there exists a line which contains at least kk points from AA, and all the points of AA on the line have the same colour?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1090.lean

Retained formal statement1 of 1

Let k3k\geq 3. Does there exist a finite set AR2A\subset \mathbb{R}^2 such that, in any 22-colouring of AA, there exists a line which contains at least kk points from AA, and all the points of AA on the line have the same colour?

Erdős [Er75f] says Graham and Selfridge proved the answer is yes when k=3k=3. Hunter has observed that, for sufficiently large nn, a generic projection of [k]n[k]^n into R2\mathbb{R}^2 has this property, by the Hales-Jewett theorem.

FormalConjectures/ErdosProblems/1090.leanErdos1090.erdos_10909 linesExact file
True  ∀ (k : ℕ),    3 ≤ kA,        ∀ (C : ↥AFin 2),S,            ∃ (hSA : SA),              Collinear ℝ ↑S                S.cardk ∧ (∀ yA, yaffineSpan ℝ ↑SyS) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : xS), Cx, ⋯⟩ = 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.

Search problems.science

Find a Problem, Result, source, or page