89.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 3 contain sorry, 0 declared as axioms

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.

Imports (1)

FormalConjecturesUtil

theorem Erdos89.erdos_89 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 sorry line 50 source
Source documentation
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.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HDiv.hDiv, Real.sqrt, Real.log, minimalDistinctDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_89 :
    (fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop]
      (fun n => (minimalDistinctDistances ℝ² n : ℝ)) := by
…
```
Mentions: minimalDistinctDistances
theorem Erdos89.erdos_89.variants.n_dvd_log_n Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances sorry line 60 source
Source documentation
Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HDiv.hDiv, Real.log, minimalDistinctDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_89.variants.n_dvd_log_n :
    (fun (n : ℕ) => n/(n : ℝ).log) =O[atTop]
      (fun n => (minimalDistinctDistances ℝ² n : ℝ)) := by
…
```
Mentions: minimalDistinctDistances
theorem Erdos89.erdos_89.variants.grid_upper_bound Documented declaration: grid_upper_bound sorry line 72 source
Source documentation
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}})$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, minimalDistinctDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, HDiv.hDiv, Real.sqrt, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_89.variants.grid_upper_bound :
    (fun n => (minimalDistinctDistances ℝ² n : ℝ)) =O[atTop]
      (fun (n : ℕ) => n/(n : ℝ).log.sqrt) := by
…
```
Mentions: minimalDistinctDistances
theorem Erdos89.erdos_89.variants.implies_n_dvd_log_n This theorem provides a sanity check, showing that the main conjecture (erdos_89) is strictly stronger than the solved Guth and Katz result line 83 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HDiv.hDiv, Real.sqrt, Real.log, minimalDistinctDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: Asymptotics.IsBigO.trans, Asymptotics.IsLittleO, Function.comp, HPow.hPow, Iff.mpr, Filter.Tendsto, Norm.norm, Asymptotics.isLittleO_one_left_iff, Filter.Tendsto.comp, tendsto_norm_atTop_atTop, tendsto_rpow_atTop, LT.lt, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv and 30 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_89.variants.implies_n_dvd_log_n (h : type_of% erdos_89) :
    type_of% erdos_89.variants.n_dvd_log_n := by
…
```
Mentions: Erdos89.erdos_89, Erdos89.erdos_89.variants.n_dvd_log_n