Erdős problem 89 · problems.science

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

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

4 retained statements2415f78e850a

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 $\frac{n}{\sqrt{\log n}}$ is the correct order if the conjecture is true: there are configurations whose number of distinct distances is $O(\frac{n}{\sqrt{\log n}})$ .

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

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

SolvedStatement only, no proof

Sources

Search problems.science