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

Asymptotic density of powerful numbers

Let $Q(x)$ denote the number of powerful integers up to $x$. Erdős and Szekeres [ES35] proved $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + O(x^{1/3}),$$ and Bateman and Grosswald [BG58] sharpened this to $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6}).$$ Improving the exponent $1/6$ in the error term unconditionally remains open; conditional improvements are known under the Riemann Hypothesis.

References:

Wikipedia
[ES35] Erdős, P. and Szekeres, G., Über die Anzahl der Abelschen Gruppen gegebener Ordnung und über ein verwandtes zahlentheoretisches Problem, Acta Sci. Math. (Szeged) 7 (1935), 95–102.
[BG58] Bateman, P. T. and Grosswald, E., On a theorem of Erdős and Szekeres, Illinois J. Math. 2 (1958), 88–98.

Imports (1)

FormalConjecturesUtil

abbrev PowerfulNumbersDensity.Q $Q(x)$ is the number of powerful integers $n$ with $1 \le n \le x$ line 45 source
Source documentation
$Q(x)$ is the number of powerful integers $n$ with $1 \le n \le x$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat
Proof uses: Set.ncard, Set.ofPred, And, LT.lt, OfNat.ofNat, Nat.Powerful, LE.le
5 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev Q (x : ℝ) : ℕ := {n : ℕ | 0 < n ∧ n.Powerful ∧ (n : ℝ) ≤ x}.ncard
```
abbrev PowerfulNumbersDensity.A The leading constant $\zeta(3/2)/\zeta(3) = 2.173\ldots$ line 48 source
Source documentation
The leading constant $\zeta(3/2)/\zeta(3) = 2.173\ldots$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, Complex.re, riemannZeta, Complex, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev A : ℝ := (riemannZeta (3 / 2)).re / (riemannZeta 3).re
```
abbrev PowerfulNumbersDensity.B The second-order constant $\zeta(2/3)/\zeta(2)$, where $\zeta(2/3)$ is given by analytic continuation line 52 source
Source documentation
The second-order constant $\zeta(2/3)/\zeta(2)$, where $\zeta(2/3)$ is given by analytic continuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, Complex.re, riemannZeta, Complex, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev B : ℝ := (riemannZeta (2 / 3)).re / (riemannZeta 2).re
…
```
theorem PowerfulNumbersDensity.asymptotic_erdos_szekeres Documented declaration: asymptotic_erdos_szekeres sorry line 60 source
Source documentation
Erdős and Szekeres [ES35] proved that the number of powerful integers up to $x$ satisfies $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + O(x^{1/3}).$$ In particular $Q(x) \sim \frac{\zeta(3/2)}{\zeta(3)} \sqrt{x}$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Real, Filter.atTop, HSub.hSub, PowerfulNumbersDensity.Q, HMul.hMul, PowerfulNumbersDensity.A, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem asymptotic_erdos_szekeres :
    (fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2)) =O[atTop]
      fun x => x ^ ((1 : ℝ) / 3) := by
…
```
Mentions: PowerfulNumbersDensity.Q, PowerfulNumbersDensity.A
theorem PowerfulNumbersDensity.asymptotic_bateman_grosswald Bateman and Grosswald [BG58] proved the sharper asymptotic $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6}).$$ sorry line 70 source
Source documentation
Bateman and Grosswald [BG58] proved the sharper asymptotic $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6}).$$

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Real, Filter.atTop, HSub.hSub, PowerfulNumbersDensity.Q, HMul.hMul, PowerfulNumbersDensity.A, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Nat, PowerfulNumbersDensity.B
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem asymptotic_bateman_grosswald :
    (fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2) - B * x ^ ((1 : ℝ) / 3)) =O[atTop]
      fun x => x ^ ((1 : ℝ) / 6) := by
…
```
Mentions: PowerfulNumbersDensity.Q, PowerfulNumbersDensity.A, PowerfulNumbersDensity.B
theorem PowerfulNumbersDensity.error_term_improvement Can the exponent $1/6$ in the error term of the Bateman–Grosswald asymptotic be improved unconditionally? sorry line 83 source
Source documentation
Can the exponent $1/6$ in the error term of the Bateman–Grosswald asymptotic be improved unconditionally? That is, is there $\delta > 0$ such that $$Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6 - \delta})?$$ Improvements are known under the Riemann Hypothesis.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Filter.atTop, HSub.hSub, PowerfulNumbersDensity.Q, HMul.hMul, PowerfulNumbersDensity.A, HPow.hPow, HDiv.hDiv, Nat, PowerfulNumbersDensity.B
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem error_term_improvement :
    answer(sorry) ↔ ∃ δ > (0 : ℝ),
      (fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2) - B * x ^ ((1 : ℝ) / 3)) =O[atTop]
        fun x => x ^ ((1 : ℝ) / 6 - δ) := by
…
```
Mentions: PowerfulNumbersDensity.Q, PowerfulNumbersDensity.A, PowerfulNumbersDensity.B