/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 89
References:
[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.
open Filteropen EuclideanGeometrynamespace Erdos89Erdős [Er46] asked whether every set of $n$ distinct points in $\mathbb{R}^2$ determines $\gg \frac{n}{\sqrt{\log n}}$ many distinct distances.
@[category research open, AMS 52]
theorem erdos_89 :
(fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop] (fun n => (minimalDistinctDistances n : ℝ)) := ⊢ (fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)
All goals completed! 🐙Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances.
@[category research solved, AMS 52]
theorem erdos_89.variants.n_dvd_log_n :
(fun (n : ℕ) => n/(n : ℝ).log) =O[atTop] (fun n => (minimalDistinctDistances n : ℝ)) := ⊢ (fun n ↦ ↑n / Real.log ↑n) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)
All goals completed! 🐙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}})$.
@[category research solved, AMS 52]
theorem erdos_89.variants.grid_upper_bound :
(fun n => (minimalDistinctDistances n : ℝ)) =O[atTop]
(fun (n : ℕ) => n/(n : ℝ).log.sqrt) := ⊢ (fun n ↦ ↑(minimalDistinctDistances n)) =O[atTop] fun n ↦ ↑n / √(Real.log ↑n)
All goals completed! 🐙
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.
h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / Real.log ↑n) =O[atTop] fun n ↦ ↑n / √(Real.log ↑n)
h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / Real.log ↑n) = fun x ↦ ↑x / Real.log ↑x * 1h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / Real.log ↑x * ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast) x
h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / Real.log ↑n) = fun x ↦ ↑x / Real.log ↑x * 1 All goals completed! 🐙
h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / Real.log ↑x * ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast) x simp_rw h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / Real.log ↑x * ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast) xh:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / Real.log ↑x * Real.log ↑x ^ (1 / 2) h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / (Real.log ↑x / Real.log ↑x ^ (1 / 2)) h:(fun n ↦ ↑n / √(Real.log ↑n)) =O[atTop] fun n ↦ ↑(minimalDistinctDistances n)this:(fun _x ↦ 1) =o[atTop] ((fun x ↦ x ^ (1 / 2)) ∘ Real.log ∘ Nat.cast)⊢ (fun n ↦ ↑n / √(Real.log ↑n)) = fun x ↦ ↑x / (Real.log ↑x / √(Real.log ↑x)) All goals completed! 🐙]-- TODO(firsching): formalize any remaining remarks from the erdosproblems.com page.
end Erdos89