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

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 670

References:

erdosproblems.com/670
[Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
[Ho26] Ho, B. S., Erdős's diameter conjecture for separated distances fails in high dimensions. arXiv:2604.15305 (2026).

Imports (1)

FormalConjecturesUtil

def Erdos670.HasSeparatedDistances A finite set line 40 source
Source documentation
A finite set $A$ of points has separated distances if all its pairwise distances differ by at least $1$: for any two different unordered pairs $\{a, b\} \neq \{c, e\}$ of distinct points of $A$, we have $\lvert d(a, b) - d(c, e)\rvert \geq 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Finset
Proof uses: Membership.mem, Ne, Sym2, Sym2.mk, LE.le, Real, OfNat.ofNat, abs, HSub.hSub, Dist.dist
11 instances, coercions and auxiliary constants left out.
```
def HasSeparatedDistances {X : Type*} [MetricSpace X] (A : Finset X) : Prop :=
…
```
theorem Erdos670.erdos_670 Let $A\subseteq \mathbb{R}^d$ be a set of $n$ points such that all pairwise distances differ by at least $1$ sorry line 54 source
Source documentation
Let $A\subseteq \mathbb{R}^d$ be a set of $n$ points such that all pairwise distances differ by at least $1$. Is the diameter of $A$ at least $(1+o(1))n^2$?
The quantifiers in the source are ambiguous. Following the remarks on erdosproblems.com, this is the regime where $d$ is fixed and the $o(1)$ term tends to $0$ as $n \to \infty$, at a rate which may depend on $d$. The case $d = 1$ was proved by Erdős (Erdos670.erdos_670.variants.dim_one), so the question is open for $d \geq 2$.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Real, GT.gt, Filter.Eventually, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos670.HasSeparatedDistances, ENNReal, HMul.hMul, HSub.hSub, HPow.hPow, Metric.diam, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_670 : answer(sorry) ↔
    ∀ d : ℕ, 1 ≤ d → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      ∀ A : Finset (EuclideanSpace ℝ (Fin d)), A.card = n → HasSeparatedDistances A →
        (1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d))) := by
…
```
Mentions: Erdos670.HasSeparatedDistances
theorem Erdos670.erdos_670.variants.dim_one Documented declaration: dim_one sorry line 66 source
Source documentation
Erdős [Er97f] proved the claim when $d = 1$: if $A\subseteq \mathbb{R}$ is a set of $n$ points such that all pairwise distances differ by at least $1$, then the diameter of $A$ is at least $(1+o(1))n^2$.

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos670.HasSeparatedDistances, ENNReal, LE.le, HMul.hMul, HSub.hSub, HPow.hPow, Metric.diam, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_670.variants.dim_one : answer(True) ↔
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      ∀ A : Finset (EuclideanSpace ℝ (Fin 1)), A.card = n → HasSeparatedDistances A →
        (1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin 1))) := by
…
```
Mentions: Erdos670.HasSeparatedDistances
theorem Erdos670.erdos_670.variants.choose_two Documented declaration: choose_two sorry line 82 source
Source documentation
The trivial lower bound: if $A\subseteq \mathbb{R}^d$ is a set of $n \neq 2$ points such that all pairwise distances differ by at least $1$, then the diameter of $A$ is at least $\binom{n}{2}$.
For $n \geq 3$, take a closest pair $a, b$ and a third point $c$. Then $1 \leq \lvert d(a, c) - d(b, c)\rvert \leq d(a, b)$, so every distance is at least $1$. The $\binom{n}{2}$ distances are at least $1$ apart, so the largest one is at least $\binom{n}{2}$. For $n = 2$ the hypothesis is vacuous, and two points at distance $1/2$ show that the bound fails.

depends on sorry what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, Erdos670.HasSeparatedDistances, OfNat.ofNat, ENNReal, Ne, Finset.card, LE.le, Nat.choose, Metric.diam
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_670.variants.choose_two (d : ℕ) (A : Finset (EuclideanSpace ℝ (Fin d)))
    (hA : HasSeparatedDistances A) (hn : A.card ≠ 2) :
    (A.card.choose 2 : ℝ) ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d))) := by
…
```
Mentions: Erdos670.HasSeparatedDistances
theorem Erdos670.erdos_670.variants.ho sorry line 99 source
depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Frequently, Nat, Exists, Finset, EuclideanSpace, Fin, HSub.hSub, HPow.hPow, And, Eq, Finset.card, Erdos670.HasSeparatedDistances, ENNReal, LE.le, Metric.diam, HMul.hMul, HAdd.hAdd and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
76 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos670.erdos_670.variants.uniform_in_dim The version of the problem where the $o(1)$ term must be uniform in the dimension $d$ has a negative answer sorry line 112 source
Source documentation
The version of the problem where the $o(1)$ term must be uniform in the dimension $d$ has a negative answer. This follows from Erdos670.erdos_670.variants.ho (Ho [Ho26]).

depends on sorry what this means
Statement uses: Iff, False, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos670.HasSeparatedDistances, ENNReal, LE.le, HMul.hMul, HSub.hSub, HPow.hPow, Metric.diam, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_670.variants.uniform_in_dim : answer(False) ↔
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ d : ℕ,
      ∀ A : Finset (EuclideanSpace ℝ (Fin d)), A.card = n → HasSeparatedDistances A →
        (1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d))) := by
…
```
Mentions: Erdos670.HasSeparatedDistances