Skip to content

Erdős problem 209

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

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

209.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/209.leanErdos209.erdos_2098 linesExact file
False ↔  ∀ (d : ℕ),    4 ≤ d →      ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))),        A.card = d →          (∀ L ∈ A, Erdos209.IsLine L) →            ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) →              (∀ (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.

Search problems.science

Find a Problem, Result, source, or page