Erdős problem 209

Let $A$ be a finite collection of $d\geq 4$ non-parallel lines in $\mathbb{R}^2$ such that there are no points where at least four lines from $A$ meet. Must there exist a 'Gallai triangle' (or 'ordinary triangle'): three lines from $A$ which intersect in three points, and each of these intersection points only intersects two lines from $A$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

209.lean

Retained formal statement1 of 1

Let $A$ be a finite collection of $d\geq 4$ non-parallel lines in $\mathbb{R}^2$ such that there are no points where at least four lines from $A$ meet. Must there exist a 'Gallai triangle' (or 'ordinary triangle'): three lines from $A$ which intersect in three points, and each of these intersection points only intersects two lines from $A$ ?

Füredi and Palásti [FuPa84] showed this is false when $d\geq 4$ is not divisible by $9$ . Escudero [Es16] showed this is false for all $d\geq 4$ .

FormalConjectures/ErdosProblems/209.leanErdos209.erdos_2098 linesExact file

1False ↔2  ∀ (d : ℕ),3    4 ≤ d →4      ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))),5        A.card = d →6          (∀ L ∈ A, Erdos209.IsLine L) →7            ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) →8              (∀ (p : EuclideanSpace ℝ (Fin 2)), Erdos209.pointMultiplicity A p ≤ 3) → Erdos209.HasGallaiTriangle A

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.