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

7 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 1000

References:

erdosproblems.com/1000
[Ca50b] Cassels, J. W. S., Some metrical theorems in Diophantine approximation. I. Proc. Cambridge Philos. Soc. (1950), 209-218.
[Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65.
[Ha] Haight, J. A., Metric Diophantine approximation and related topics. PhD thesis.

Imports (1)

FormalConjecturesUtil

def Erdos1000.phiSeq Given an infinite sequence of positive integers line 47 source
Source documentation
Given an infinite sequence of positive integers $A = \{n_1 < n_2 < \cdots\}$, phiSeq n k is $\phi_A(k)$: the number of $1\leq m\leq n_k$ such that $\frac{m}{n_k}$ cannot be written as $\frac{b}{n_j}$ for any integer $b$ and any $1\leq j<k$; equivalently, $$ \frac{n_k}{(m,n_k)}\nmid n_j $$ for all $1\leq j<k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset.filter, LT.lt, Not, Dvd.dvd, HDiv.hDiv, Nat.gcd, Finset.Icc, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
def phiSeq (n : ℕ → ℕ) (k : ℕ) : ℕ :=
…
```
def Erdos1000.phiAvg The average $\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}$ line 53 source
Source documentation
The average $\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, Finset.sum, Finset.range, Erdos1000.phiSeq
6 instances, coercions and auxiliary constants left out.
```
noncomputable def phiAvg (n : ℕ → ℕ) (N : ℕ) : ℝ :=
…
```
theorem Erdos1000.erdos_1000 Documented declaration: erdos_1000 sorry line 74 source
Source documentation
Let $A=\{n_1<n_2<\cdots\}$ be an infinite sequence of positive integers, and let $\phi_A(k)$ count the number of $1\leq m\leq n_k$ such that the fraction $\frac{m}{n_k}$ cannot be written as $\frac{b}{n_j}$ for any integer $b$ and any $j<k$; equivalently, $$ \frac{n_k}{(m,n_k)}\nmid n_j $$ for all $1\leq j<k$.
Is there a sequence $A$ such that $$ \lim_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0? $$
This was solved by Haight [Ha] who proved that such a sequence does exist (contrary to Erdős' expectations).

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, StrictMono, LT.lt, OfNat.ofNat, Filter.Tendsto, Real, Erdos1000.phiAvg, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1000 : answer(True) ↔
    ∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
      Tendsto (phiAvg n) atTop (𝓝 0) := by
…
```
Mentions: Erdos1000.phiAvg
theorem Erdos1000.erdos_1000.variants.totient_le It is trivial that $\phi_A(k)\geq \phi(n_k)$, where $\phi$ is the Euler totient function line 83 source
Source documentation
It is trivial that $\phi_A(k)\geq \phi(n_k)$, where $\phi$ is the Euler totient function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, StrictMono, LT.lt, OfNat.ofNat, LE.le, Nat.totient, Erdos1000.phiSeq
Proof uses: Eq.mpr, Finset.card, Finset.filter, Nat.Coprime, Finset.range, id, Eq, congrArg, Nat.totient.eq_1, Not, Dvd.dvd, HDiv.hDiv, Nat.gcd, Finset.Icc, Erdos1000.phiSeq.eq_1, Finset.card_le_card_of_injOn, ite, Membership.mem, Set, Finset and 31 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1000.variants.totient_le (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0)
    (k : ℕ) :
    (n k).totient ≤ phiSeq n k := by
…
```
Mentions: Erdos1000.phiSeq
theorem Erdos1000.erdos_1000.variants.liminf_eq_zero Documented declaration: liminf_eq_zero sorry line 130 source
Source documentation
The study of $\phi_A$ was introduced by Cassels [Ca50b], who proved that there exist sequences such that $$ \liminf_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0. $$

depends on sorry what this means
Statement uses: Exists, Nat, And, StrictMono, LT.lt, OfNat.ofNat, Eq, Real, Filter.liminf, Erdos1000.phiAvg, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1000.variants.liminf_eq_zero :
    ∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
      atTop.liminf (phiAvg n) = 0 := by
…
```
Mentions: Erdos1000.phiAvg
theorem Erdos1000.erdos_1000.variants.not_tendsto_zero Erdős [Er64b] proved that the limit of $\frac{\phi_A(k)}{n_k}$ as $k\to \infty$ cannot be $0$ sorry line 139 source
Source documentation
Erdős [Er64b] proved that the limit of $\frac{\phi_A(k)}{n_k}$ as $k\to \infty$ cannot be $0$.

depends on sorry what this means
Statement uses: Nat, StrictMono, LT.lt, OfNat.ofNat, Not, Filter.Tendsto, Real, HDiv.hDiv, Erdos1000.phiSeq, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1000.variants.not_tendsto_zero (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0) :
    ¬ Tendsto (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) atTop (𝓝 0) := by
…
```
Mentions: Erdos1000.phiSeq
theorem Erdos1000.erdos_1000.variants.limsup_eq_one In fact he proved that if $\liminf \frac{\phi_A(k)}{n_k}=0$ then $\limsup \frac{\phi_A(k)}{n_k}=1$ sorry line 148 source
Source documentation
In fact he proved that if $\liminf \frac{\phi_A(k)}{n_k}=0$ then $\limsup \frac{\phi_A(k)}{n_k}=1$.

depends on sorry what this means
Statement uses: Nat, StrictMono, LT.lt, OfNat.ofNat, Eq, Real, Filter.liminf, HDiv.hDiv, Erdos1000.phiSeq, Filter.atTop, Filter.limsup
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1000.variants.limsup_eq_one (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0)
    (h : atTop.liminf (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 0) :
    atTop.limsup (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 1 := by
…
```
Mentions: Erdos1000.phiSeq