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

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?

This has been disproved by Xichuan in the comments, who has found three explicit counterexamples.

FormalConjectures/ErdosProblems/105.leanErdos105.erdos_1053 linesExact file
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}
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.