Erdős problem 89

Erdős [Er46] asked whether every set of $n$ distinct points in $\mathbb{R}^2$ determines $\gg \frac{n}{\sqrt{\log n}}$ many distinct distances.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

89.lean

Retained formal statement4 of 4

Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances.

FormalConjectures/ErdosProblems/89.leanErdos89.erdos_89.variants.n_dvd_log_n1 lineExact file

1(fun n => ↑n / Real.log ↑n) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)

SolvedStatement only, no proof