Skip to content

Erdős problem 100

Start work

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

100.lean

Retained formal statement3 of 5

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

FormalConjectures/ErdosProblems/100.leanErdos100.erdos_100.variants.guth_katz4 linesExact file
∃ C > 0,  ∀ᶠ (n : ℕ) in Filter.atTop,    ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),      A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A ≥ C * ↑n / Real.log ↑n
SolvedStatement only, no proof