Skip to content

Erdős problem 209

Let AA be a finite collection of d4d\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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/209.lean

Formal Conjectures

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

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:209

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page