Erdős problem 105
Let be disjoint sets of size and respectively, with not all of contained on a single line. Is there a line which contains at least two points from and no points from ?
Sources
FormalConjectures/ErdosProblems/
105.lean
Retained formal statement
Let be disjoint sets of size and respectively, with not all of contained on a single line. Is there a line which contains at least two points from and no points from ?
This has been disproved by Xichuan in the comments, who has found three explicit counterexamples.
False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}