Erdős problem 1090

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

1090.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/1090.leanErdos1090.erdos_10909 linesExact file

1True ↔2  ∀ (k : ℕ),3    3 ≤ k →4      ∃ A,5        ∀ (C : ↥A → Fin 2),6          ∃ S,7            ∃ (hSA : S ⊆ A),8              Collinear ℝ ↑S ∧9                S.card ≥ k ∧ (∀ y ∈ A, y ∈ affineSpan ℝ ↑S → y ∈ S) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : x ∈ S), C ⟨x, ⋯⟩ = 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.