Erdős problem 98 · problems.science

Let $h(n)$ be such that any $n$ points in $\mathbb{R}^2$ , with no three on a line and no four on a circle, determine at least $h(n)$ distinct distances. Does $h(n)/n\to \infty$ ?

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

98.lean

Retained formal statement2 of 2

Erdős could not even prove $h(n)\geq n$ . Pach has shown $h(n) < n^{\log_2 3}$ . Erdős, Füredi, and Pach [EFPR93] have improved this to $h(n) < n\exp(c\sqrt{\log n})$ for some constant $c>0$ .

FormalConjectures/ErdosProblems/98.leanErdos98.erdos_98.variants.upper_bound1 lineExact file

1∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos98.h n) < ↑n * Real.exp (c * √(Real.log ↑n))

SolvedStatement only, no proof

Sources

Search problems.science