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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/89.lean

Formal Conjectures

FormalConjectures/ErdosProblems/89.leanErdos89.erdos_891 lineExact file

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

OpenStatement only, no proof