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 statement3 of 4

A construction of Hickerson shows that this fails with n−2n-2.

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