Erdős problem 209
Let be a finite collection of non-parallel lines in such that there are no points where at least four lines from meet. Must there exist a 'Gallai triangle' (or 'ordinary triangle'): three lines from which intersect in three points, and each of these intersection points only intersects two lines from ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/209.leanFalse ↔ ∀ (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 AProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:209
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine