Erdős problem 105 · problems.science

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

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

105.lean

Retained formal statement3 of 4

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

FormalConjectures/ErdosProblems/105.leanErdos105.erdos_105.variants.hickerson2 linesExact file

1¬∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))),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

Sources

Search problems.science