448.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, 5 contain sorry, 0 declared as axioms

Erdős Problem 448

References:

erdosproblems.com/448
OEIS A397433: the integer sequence $\tau^+(n)$ (the constant $\alpha$ in Ford's asymptotic is OEIS A074738).
[Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70.
[Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82.
[HaTe88] Hall, Richard R. and Tenenbaum, Gérald, Divisors. (1988), xvi+167.
[ErTe81] Erdős, P., Tenenbaum, G., Sur la structure de la suite des diviseurs d'un entier. Ann. Inst. Fourier (Grenoble) 31 (1981), 17–37.
[Fo08] Ford, Kevin, The distribution of integers with a divisor in a given interval. Ann. of Math. (2) 168 (2008), 367–433.
[Te13] Tenenbaum, Gérald, Some of Erdős' unconventional problems in number theory, thirty-four years later. Erdős Centennial, Bolyai Soc. Math. Stud. 25 (2013), 651–681.

Imports (1)

FormalConjecturesUtil

def Erdos448.tauPlus tauPlus n (written $\tau^+(n)$) counts the number of $k$ such that $n$ has a divisor in $[2^k, 2^{k+1})$ line 47 source
Source documentation
tauPlus n (written $\tau^+(n)$) counts the number of $k$ such that $n$ has a divisor in $[2^k, 2^{k+1})$. Equivalently, the number of distinct values $\lfloor \log_2 d \rfloor$ as $d$ ranges over the divisors of $n$: a divisor $d$ lies in $[2^k, 2^{k+1})$ iff Nat.log 2 d = k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset.image, Nat.log, OfNat.ofNat, Nat.divisors
2 instances, coercions and auxiliary constants left out.
```
def tauPlus (n : ℕ) : ℕ := (n.divisors.image (Nat.log 2)).card
…
```
theorem Erdos448.tauPlus_six Sanity check: $\tau^+(6) = 3$ line 52 source
Source documentation
Sanity check: $\tau^+(6) = 3$. Divisors $1, 2, 3, 6$ lie in dyadic blocks $k = 0, 1, 1, 2$, so the distinct blocks are $\{0, 1, 2\}$. ($\tau(6) = 4$.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos448.tauPlus, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem tauPlus_six : tauPlus 6 = 3 := by decide
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.tauPlus_twelve Sanity check: $\tau^+(12) = 4$ line 57 source
Source documentation
Sanity check: $\tau^+(12) = 4$. Divisors $1, 2, 3, 4, 6, 12$ lie in dyadic blocks $k = 0, 1, 1, 2, 2, 3$, so the distinct blocks are $\{0, 1, 2, 3\}$. ($\tau(12) = 6$.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos448.tauPlus, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem tauPlus_twelve : tauPlus 12 = 4 := by decide
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.tauPlus_le_tau Always $\tau^+(n) \le \tau(n)$: the occupied dyadic blocks are the image of the divisor set under Nat.log 2, and an image has at most as many elements as its source line 63 source
Source documentation
Always $\tau^+(n) \le \tau(n)$: the occupied dyadic blocks are the image of the divisor set under Nat.log 2, and an image has at most as many elements as its source. This is what makes the $\epsilon < 1$ comparison in the problem meaningful.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos448.tauPlus, Finset.card, Nat.divisors
Proof uses: Finset.card_image_le, Nat.log, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
theorem tauPlus_le_tau (n : ℕ) : tauPlus n ≤ n.divisors.card :=
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.erdos_448 sorry line 85 source
depends on sorry what this means
Statement uses: Iff, False, Real, LT.lt, OfNat.ofNat, Set.HasDensity, Nat, Set.ofPred, Erdos448.tauPlus, HMul.hMul, Finset.card, Nat.divisors, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos448.erdos_448.variants.erdos_tenenbaum Quantitative form of the (negative) answer to erdos_448 sorry line 96 source
Source documentation
Quantitative form of the (negative) answer to erdos_448. Erdős and Tenenbaum [ErTe81] showed that the upper density of $\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}$ is in fact $\asymp \epsilon^{1 - o(1)}$, where the $o(1)$ in the exponent tends to $0$ as $\epsilon \to 0$. Equivalently, $\log(\text{upper density}) / \log \epsilon \to 1$ as $\epsilon \to 0^+$.

depends on sorry what this means
Statement uses: Filter.Tendsto, Real, HDiv.hDiv, Real.log, Set.upperDensity, Nat, Set.ofPred, LT.lt, Erdos448.tauPlus, HMul.hMul, Finset.card, Nat.divisors, Set.univ, nhdsWithin, OfNat.ofNat, Set.Ioi, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
41 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_448.variants.erdos_tenenbaum :
    Tendsto
      (fun ε : ℝ =>
        Real.log ({n : ℕ | (tauPlus n : ℝ) < ε * (n.divisors.card : ℝ)}.upperDensity) / Real.log ε)
      (𝓝[>] (0 : ℝ)) (𝓝 (1 : ℝ)) := by
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.erdos_448.variants.hall_tenenbaum_upper_bound Documented declaration: hall_tenenbaum_upper_bound sorry line 108 source
Source documentation
A more precise result of Hall and Tenenbaum [HaTe88, §4.6]: the upper density of $\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}$ is $\ll \epsilon \cdot \log(2/\epsilon)$ as $\epsilon \to 0^+$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Real, nhdsWithin, OfNat.ofNat, Set.Ioi, Set.upperDensity, Nat, Set.ofPred, LT.lt, Erdos448.tauPlus, HMul.hMul, Finset.card, Nat.divisors, Set.univ, Real.log, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_448.variants.hall_tenenbaum_upper_bound :
    (fun ε : ℝ => ({n : ℕ | (tauPlus n : ℝ) < ε * (n.divisors.card : ℝ)}).upperDensity)
      =O[𝓝[>] (0 : ℝ)] (fun ε : ℝ => ε * Real.log (2 / ε)) := by
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.erdos_448.variants.hall_tenenbaum_distribution Documented declaration: hall_tenenbaum_distribution sorry line 120 source
Source documentation
Hall and Tenenbaum [HaTe88] further prove that $\tau^+(n)/\tau(n)$ has a distribution function: there is a distribution function F (non-decreasing, with $F(-\infty) = 0$ and $F(+\infty) = 1$) such that, for every continuity point $z$ of F, the set $\{n : \tau^+(n)/\tau(n) \le z\}$ has density F z. Tenenbaum [Te13] proved that F is continuous at $z = 1$ and asked to determine its discontinuity points, if any.

depends on sorry what this means
Statement uses: Exists, Real, And, Monotone, Filter.Tendsto, Filter.atBot, nhds, OfNat.ofNat, Filter.atTop, ContinuousAt, Set.HasDensity, Nat, Set.ofPred, LE.le, HDiv.hDiv, Erdos448.tauPlus, Finset.card, Nat.divisors, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_448.variants.hall_tenenbaum_distribution :
    ∃ F : ℝ → ℝ, Monotone F ∧ Tendsto F atBot (𝓝 0) ∧ Tendsto F atTop (𝓝 1) ∧
      ∀ z : ℝ, ContinuousAt F z →
        {n : ℕ | (tauPlus n : ℝ) / (n.divisors.card : ℝ) ≤ z}.HasDensity (F z) := by
…
```
Mentions: Erdos448.tauPlus
theorem Erdos448.erdos_448.variants.ford Erdős and Graham asked whether there is a good inequality for $\sum_{n \le x} \tau^+(n)$ sorry line 132 source
Source documentation
Erdős and Graham asked whether there is a good inequality for $\sum_{n \le x} \tau^+(n)$. This was answered by Ford [Fo08], who proved $$ \sum_{n \le x} \tau^+(n) \asymp x \cdot \frac{(\log x)^{1 - \alpha}}{(\log\log x)^{3/2}}, $$ where $\alpha = 1 - \frac{1 + \log\log 2}{\log 2} = 0.08607\ldots$.

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Finset.sum, Finset.Icc, OfNat.ofNat, Erdos448.tauPlus, HSub.hSub, HDiv.hDiv, HAdd.hAdd, Real.log, HMul.hMul, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_448.variants.ford :
    (fun x : ℕ => ∑ n ∈ Finset.Icc 1 x, (tauPlus n : ℝ))
      =Θ[atTop]
      (fun x : ℕ =>
        let α : ℝ := 1 - (1 + Real.log (Real.log 2)) / Real.log 2
…
```
Mentions: Erdos448.tauPlus