Erdős Problem 89

References:

• erdosproblems.com/89
• [Er46] Erdős, Paul. On sets of distances of $n$ points. Amer. Math. Monthly 53 (1946), 248--250.
• [GuKa15] Guth, Larry and Katz, Nets Hawk. On the Erdős distinct distances problem in the plane. Ann. of Math. (2) 181 (2015), 155--190.
• [Mo52] Moser, Leo. On the different distances determined by $n$ points. Amer. Math. Monthly 59 (1952), 85--91.

AI disclosure

Lean 4 code in this file was drafted with assistance from OpenAI Codex. The mathematical content and references are the author's own work.

theorem Erdos89.erdos_89 : (fun (n : ℕ) => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun (n : ℕ) => ↑(EuclideanGeometry.minimalDistinctDistances n)

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.

theorem Erdos89.erdos_89.variants.n_dvd_log_n : (fun (n : ℕ) => ↑n / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(EuclideanGeometry.minimalDistinctDistances n)

Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances.

theorem Erdos89.erdos_89.variants.grid_upper_bound : (fun (n : ℕ) => ↑(EuclideanGeometry.minimalDistinctDistances n)) =O[Filter.atTop] fun (n : ℕ) => ↑n / √(Real.log ↑n)

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

theorem Erdos89.erdos_89.variants.implies_n_dvd_log_n (h : (fun (n : ℕ) => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun (n : ℕ) => ↑(EuclideanGeometry.minimalDistinctDistances n)) : (fun (n : ℕ) => ↑n / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(EuclideanGeometry.minimalDistinctDistances n)

This theorem provides a sanity check, showing that the main conjecture (erdos_89) is strictly stronger than the solved Guth and Katz result. It proves that, trivially, if the lower bound $\frac{n}{\sqrt{\log n}}$ holds, then the weaker lower bound $\frac{n}{\log n}$ must also hold.