Erdős problem 100
From [Piepmeyer]: 9 points with diameter . TODO: find reference
Sources
FormalConjectures/ErdosProblems/
100.lean
Retained formal statement
Is the diameter of at least for some constant ?
True ↔ ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑nOpenStatement only, no proof