Erdős problem 1090
Let . Does there exist a finite set such that, in any -colouring of , there exists a line which contains at least points from , and all the points of on the line have the same colour?
Sources
FormalConjectures/ErdosProblems/
1090.lean
Retained formal statement
Let . Does there exist a finite set such that, in any -colouring of , there exists a line which contains at least points from , and all the points of on the line have the same colour?
Erdős [Er75f] says Graham and Selfridge proved the answer is yes when . Hunter has observed that, for sufficiently large , a generic projection of into has this property, by the Hales-Jewett theorem.
True ↔ ∀ (k : ℕ), 3 ≤ k → ∃ A, ∀ (C : ↥A → Fin 2), ∃ S, ∃ (hSA : S ⊆ A), Collinear ℝ ↑S ∧ S.card ≥ k ∧ (∀ y ∈ A, y ∈ affineSpan ℝ ↑S → y ∈ S) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : x ∈ S), C ⟨x, ⋯⟩ = c