Erdős problem 100
From [Piepmeyer]: 9 points with diameter . TODO: find reference
Sources
FormalConjectures/ErdosProblems/
100.lean
Retained formal statement
From [Kanold]: diameter . TODO: find reference
∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A ≥ ↑n ^ (3 / 4)SolvedStatement only, no proof