Erdős Problem 98

References:

• [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108.
• [Er83c] Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54.
• [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177.
• [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478.
• [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240.
• [EFPR93] Erdős, Paul and Füredi, Zoltán and Pach, János and Ruzsa, Imre Z., The grid revisited. Discrete Math. (1993), 189-196.
• [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
• [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537.
• erdosproblems.com/98

noncomputable def Erdos98.h (n : ℕ) : ℕ

$h(n)$ is the minimum number of distinct distances determined by any $n$-point set in $\mathbb{R}^2$ in general position (no three collinear, no four cocyclic).

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos98.erdos_98 : True ↔ Filter.Tendsto (fun (n : ℕ) => ↑(h n) / ↑n) Filter.atTop Filter.atTop

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$?

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

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$.