Skip to content

Erdős problem 105

Start work

Let A,B⊂R2A,B\subset \mathbb{R}^2 be disjoint sets of size nn and n−3n-3 respectively, with not all of AA contained on a single line. Is there a line which contains at least two points from AA and no points from BB?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

105.lean

Retained formal statement2 of 4

A result independently proved by Beck [Be83] and Szemerédi and Trotter [SzTr83] (see [211]) implies it is true with n−3n-3 replaced by cncn for some constant c>0c>0.

FormalConjectures/ErdosProblems/105.leanErdos105.erdos_105.variants.beck_szemeredi_trotter3 linesExact file
∃ c > 0,  ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))),    Disjoint A B → ↑B.card ≤ c * ↑A.card → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}
SolvedStatement only, no proof