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

References:

erdosproblems.com/946
[ErMi52] Erdős, P. and Mirsky, L., The distribution of values of the divisor function {$d(n)$}. Proc. London Math. Soc. (3) (1952), 257--271.
[Sp81] Spiro, C. A., The frequency with which an integral-valued, prime-independent, multiplicative or additive function of n divides a polynomial function of n.
[He84] Heath-Brown, D. R., The divisor function at consecutive integers. Mathematika 31 (1984), no. 2, 141--149.
[Hi85] Hildebrand, A., The divisor function at consecutive integers. Pacific J. Math. (1987), 307--319
[EPS87] Erdős, P., Pomerance, C., and Sarkőzy, A., On locally repeated values of arithmetic functions. III. Proc. Amer. Math. Soc. (1987), 1--7.

Imports (1)

FormalConjecturesUtil

theorem Erdos946.erdos_946 sorry line 51 source
depends on sorry what this means
Statement uses: Set.Infinite, Nat, Set.ofPred, Eq, ArithmeticFunction, ArithmeticFunction.sigma, OfNat.ofNat, HAdd.hAdd
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 Erdos946.erdos_946.variants.spiro_5040 There are infinitely many $n$ such that $τ(n) = τ(n + 5040)$ sorry line 58 source
Source documentation
There are infinitely many $n$ such that $τ(n) = τ(n + 5040)$. Proved in [Sp81].

depends on sorry what this means
Statement uses: Set.Infinite, Nat, Set.ofPred, Eq, ArithmeticFunction, ArithmeticFunction.sigma, OfNat.ofNat, HAdd.hAdd
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_946.variants.spiro_5040 : {n : ℕ | σ 0 n = σ 0 (n + 5040)}.Infinite := by
…
```
def Erdos946.erdos946Count Number of $n \le x$ with $τ(n) = τ(n+1)$ line 62 source
Source documentation
Number of $n \le x$ with $τ(n) = τ(n+1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Finset.card, Nat, Finset.filter, Eq, ArithmeticFunction, ArithmeticFunction.sigma, OfNat.ofNat, HAdd.hAdd, Finset.range, Nat.floor
16 instances, coercions and auxiliary constants left out.
```
noncomputable def erdos946Count (x : ℝ) : ℝ :=
…
```
theorem Erdos946.erdos_946.variants.heathbrown_lower_bound The number of $n \le x$ with $τ(n) = τ(n+1)$ is at least $x / (\log x)^7$ for all sufficiently large $x$ sorry line 70 source
Source documentation
The number of $n \le x$ with $τ(n) = τ(n+1)$ is at least $x / (\log x)^7$ for all sufficiently large $x$. Proved in [He84].

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Real, Filter.atTop, HDiv.hDiv, HPow.hPow, Nat, Real.log, OfNat.ofNat, Erdos946.erdos946Count
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_946.variants.heathbrown_lower_bound :
    (fun x => x / (x.log)^7) =O[atTop] erdos946Count := by
…
```
Mentions: Erdos946.erdos946Count
theorem Erdos946.erdos_946.variants.hildebrand_lower_bound Improved lower bound in [Hi85]: $Ω(x / (\log \log x)^3)$ sorry line 78 source
Source documentation
Improved lower bound in [Hi85]: $Ω(x / (\log \log x)^3)$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Real, Filter.atTop, HDiv.hDiv, HPow.hPow, Nat, Real.log, OfNat.ofNat, Erdos946.erdos946Count
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_946.variants.hildebrand_lower_bound :
    (fun x => x / (x.log.log)^3) =O[atTop] erdos946Count := by
…
```
Mentions: Erdos946.erdos946Count
theorem Erdos946.erdos_946.variants.upper_bound Upper bound in [EPS87]: $O(x / \sqrt{\log \log x})$ sorry line 86 source
Source documentation
Upper bound in [EPS87]: $O(x / \sqrt{\log \log x})$.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_946.variants.upper_bound : erdos946Count =O[atTop] (fun x => x / √x.log.log ) := by
…
```
Mentions: Erdos946.erdos946Count