On the Erdős Conjecture on Consecutive Powerful Numbers

This preprint provides an exhaustive mathematical treatise on Erdős Problem #27 regarding the additive distribution of powerful numbers. A positive integer $n \in \mathbb{N}_{\ge 1}$ is defined to be powerful (or $2$-full / square-full) if every prime divisor divides it to at least the second power: $$p \mid n \implies p^2 \mid n$$ Paul Erdős conjectured the existence of infinitely many pairs of consecutive powerful numbers $(n, n+1)$ and investigated the existence and bounds of longer consecutive sequences. Key Mathematical Results & Contributions Canonical Factorization Theorem: Complete, rigorous proof of the existence and uniqueness of the canonical representation $n = a^2 b^3$ where $b$ is squarefree ($\mu^2(b) = 1$), derived step-by-step via the Euclidean division of $p$-adic exponents ($e_i = 2q_i + r_i$). Minimal Consecutive Pair: Exact algebraic verification of the minimal pair $(8, 9) = (2^3, 3^2)$. Pellian Diophantine Reduction in $\mathbb{Z}[\sqrt{2}]$: Demonstration that every solution to the Pell equation $x^2 - 8y^2 = 1$ generated by the fundamental unit $\epsilon_0 = 3 + 2\sqrt{2} \in \mathcal{O}_{\mathbb{Q}(\sqrt{2})}^\times$ yields an infinite sequence of distinct consecutive powerful pairs $(8y_k^2, x_k^2)$, with explicit computations and prime factorizations for the first six terms. Modulo 4 Obstruction Principle: Arithmetic proof that any integer $m \equiv 2 \pmod 4$ has a $2$-adic valuation of exactly $v_2(m) = 1$, rendering it unconditionally non-powerful. Four Consecutive Impossibility Theorem: Exhaustive partition proof over the four residue classes modulo $4$, establishing that among any four consecutive integers $(n, n+1, n+2, n+3)$, exactly one is congruent to $2 \pmod 4$. This rigorously proves that no four consecutive powerful numbers can ever exist in $\mathbb{N}$. Three Consecutive Modulo 4 Constraint & $abc$ Conjecture: Proof that any hypothetical triplet $(n, n+1, n+2)$ must strictly satisfy $n \equiv 3 \pmod 4$, accompanied by Granville's heuristic proving the finiteness of consecutive triplets under the $abc$ conjecture. 100% Machine-Checked Verification in Lean 4 Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub: https://github. com/flouzzy/erdos-problems Primary MSC (2020): 11A51, 11D09, 11B83, 11D45, 68V20.Keywords: Erdős Problem #27, Powerful Numbers, 2-Full Integers, Diophantine Equations, Pell Equation, abc Conjecture, Formal Verification, Lean 4, Mathlib.