Skip to content

Erdős problem 98

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

98.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/98.leanErdos98.erdos_98.variants.upper_bound1 lineExact file
∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos98.h n) < ↑n * Real.exp (c * √(Real.log ↑n))
SolvedStatement only, no proof