Skip to content

Erdős problem 89

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

89.lean

Retained formal statement2 of 4

The square grid construction, going back to Erdős and Moser, shows that nlog⁡n\frac{n}{\sqrt{\log n}} is the correct order if the conjecture is true: there are configurations whose number of distinct distances is O(nlog⁡n)O(\frac{n}{\sqrt{\log n}}).

FormalConjectures/ErdosProblems/89.leanErdos89.erdos_89.variants.grid_upper_bound1 lineExact file
(fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)
SolvedStatement only, no proof