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

9 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 170

Reference: erdosproblems.com/170

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Wikipedia/SparseRuler.lean

def Erdos170.PerfectRuler Documented declaration: PerfectRuler line 36 source
Source documentation
An $N$-perfect ruler is a finite subset $A \subseteq \mathbb{N}$ (the marks), such that each positive integer $k \leq N$ can be measured, that is, expressed as a difference $k = a_1 - a_0$ with $a_0, a_1 \in A$. The set $A$ is then also called a difference basis w.r.t. $N$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Membership.mem, Finset.range, HAdd.hAdd, OfNat.ofNat, Exists, And, Eq, HSub.hSub
7 instances, coercions and auxiliary constants left out.
```
def PerfectRuler (N : ℕ) (A : Finset ℕ) : Prop :=
…
```
def Erdos170.PerfectRulersLengthN We define the set of all $N$-perfect rulers $A$ of length $N$, i.e. subsets $A \subseteq \{0, \dots, N\}$, s.t line 42 source
Source documentation
We define the set of all $N$-perfect rulers $A$ of length $N$, i.e. subsets $A \subseteq \{0, \dots, N\}$, s.t. $A$ is $N$-perfect. This is also called a restricted difference basis w.r.t. $N$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, Erdos170.PerfectRuler, Finset.range, HAdd.hAdd, OfNat.ofNat, Membership.mem, Exists, And, Eq, HSub.hSub, Finset.powerset
10 instances, coercions and auxiliary constants left out.
```
def PerfectRulersLengthN (N : ℕ) :
    Finset (Finset ℕ) := (Finset.range (N + 1)).powerset.filter (PerfectRuler N)
```
Mentions: Erdos170.PerfectRuler
abbrev Erdos170.TrivialRuler The trivial ruler with all marks $\{0, \dots, N\}$ line 46 source
Source documentation
The trivial ruler with all marks $\{0, \dots, N\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.range, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev TrivialRuler (N : ℕ) : Finset ℕ := Finset.range (N+1)
…
```
lemma Erdos170.trivial_ruler_is_perfect Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$ line 50 source
Source documentation
Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Erdos170.PerfectRulersLengthN, Erdos170.TrivialRuler
Proof uses: Eq.mpr, And, LT.lt, HAdd.hAdd, OfNat.ofNat, Finset.range, Erdos170.PerfectRuler, id, Eq, Eq.trans, Finset.filter, Exists, HSub.hSub, Finset.powerset, congrFun', congrArg, LE.le, And.intro, of_eq_true, True and 5 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma trivial_ruler_is_perfect (N : ℕ) : TrivialRuler N ∈ PerfectRulersLengthN N := by
…
```
Mentions: Erdos170.TrivialRuler, Erdos170.PerfectRulersLengthN
def Erdos170.F We define a function F N as the minimum cardinality of an N-perfect ruler of length N line 55 source
Source documentation
We define a function F N as the minimum cardinality of an N-perfect ruler of length N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.min', Finset.image, Finset, Finset.card, Erdos170.PerfectRulersLengthN
3 instances, coercions and auxiliary constants left out.
```
def F (N : ℕ) : ℕ :=
…
```
lemma Erdos170.erdos170 The problem is to determine the limit of the sequence $\frac{F(N)}{\sqrt{N}}$ as $N \to \infty$ sorry line 61 source
Source documentation
The problem is to determine the limit of the sequence $\frac{F(N)}{\sqrt{N}}$ as $N \to \infty$.

depends on sorry what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Erdos170.F, Real.sqrt, Filter.atTop, nhds, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma erdos170 : Filter.Tendsto (fun N => F N / √N) Filter.atTop (𝓝 answer(sorry)) := by sorry
```
Mentions: Erdos170.F
abbrev Erdos170.lower_bound A known lower bound to the limit by Leech [Le56], which is $1.56\dots$ line 64 source
Source documentation
A known lower bound to the limit by Leech [Le56], which is $1.56\dots$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Real.sqrt, SupSet.sSup, Set.ofPred, Exists, And, Ne, OfNat.ofNat, Eq, HMul.hMul, HSub.hSub, HDiv.hDiv, Real.sin
15 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev lower_bound := √(sSup {2 * (1 - Real.sin θ / θ) | θ ≠ 0})
```
abbrev Erdos170.upper_bound A known upper bound obtained by constructing Wichmann's Rulers [Wi63] line 66 source
Source documentation
A known upper bound obtained by constructing Wichmann's Rulers [Wi63].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Real.sqrt, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev upper_bound := √3
…
```
lemma Erdos170.erdos170.existing_bounds The existence of the limit has been proved by Erdős and Gál [ErGa48] sorry line 72 source
Source documentation
The existence of the limit has been proved by Erdős and Gál [ErGa48]. The lower bound has been proven by Leech [Le56], who refined an argument of Rédei and Rényi. The upper bound is due to Wichmann [Wi63].

depends on sorry what this means
Statement uses: Exists, Real, And, Membership.mem, Set, Set.Icc, Erdos170.lower_bound, Erdos170.upper_bound, Filter.Tendsto, Nat, HDiv.hDiv, Erdos170.F, Real.sqrt, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma erdos170.existing_bounds :
  ∃ x ∈ Set.Icc lower_bound upper_bound,
    Filter.Tendsto (fun N => F N / √N) Filter.atTop (𝓝 x) := by sorry
…
```
Mentions: Erdos170.lower_bound, Erdos170.upper_bound, Erdos170.F