Skip to content

Asymptotic Density of Powerful Numbers #3686

@franzhusch

Description

@franzhusch

What is the conjecture

A positive integer $n$ is powerful if for every prime $p$ dividing $n$, we have $p^2 \mid n$. Let $Q(x)$ denote the number of powerful integers up to $x$. The Asymptotic Density of Powerful Numbers conjecture states that:

$$Q(x) = \zeta(1/2)^{-1} \sqrt{x} + o(\sqrt{x})$$

where $\zeta$ is the Riemann zeta function and $\zeta(1/2)^{-1} \approx 0.3039$. Equivalently, the natural density of powerful numbers is $\zeta(1/2)^{-1}$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

Prerequisites needed

Formalizability Rating: 2/5 (0 is best) (as of 2026-04-03)

Building blocks (from search results):

  • Nat.Prime and divisibility theory (foundational in Mathlib)
  • Complex.zeta function (available in Mathlib)
  • Asymptotic notation o(...) (available via Asymptotics in Mathlib)

Missing pieces:

  • IsPowerful predicate definition for integers where all prime factors appear with exponent ≥ 2 (not in Mathlib; similar to Powerfree in formal-conjectures repo but inverse property)
  • Formal asymptotic density definition and convergence theory for counting functions (requires new definitions connecting divisor/factor theory to asymptotic analysis)

Rating justification: The core definitions (primes, divisibility, zeta function) are present in Mathlib, but formalizing powerful numbers as a predicate and connecting the counting function $Q(x)$ to asymptotic analysis requires moderate infrastructure development beyond simple composition of existing concepts.

AMS categories

  • ams-11

Choose either option

  • I plan on adding this conjecture to the repository
  • This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions