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

It remains possible that this holds with n−4n-4 (or in general with n−O(1)n-O(1) or (1−o(1))n(1-o(1))n).

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