Erdős problem 100 · problems.science

From [Piepmeyer]: 9 points with diameter $< 5$ . TODO: find reference

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

100.lean

Retained formal statement3 of 5

From [GuKa15]: diameter $\gg n / \log n$ .

FormalConjectures/ErdosProblems/100.leanErdos100.erdos_100.variants.guth_katz4 linesExact file

1∃ C > 0,2  ∀ᶠ (n : ℕ) in Filter.atTop,3    ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),4      A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A ≥ C * ↑n / Real.log ↑n

SolvedStatement only, no proof

Sources

Search problems.science