A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below $10^{14}$

Abstract

Erdős problem 364 asks whether three consecutive powerful numbers exist, where $n$ is powerful if $p \mid n$ implies $p^2 \mid n$. Erdős (1976) and, independently, Mollin and Walsh (1986) conjectured that none do; the $abc$ conjecture implies at most finitely many. The conjecture remains open. We present the first verification of the conjecture at any finite bound that is checked end to end by a proof kernel: machine-checked theorems in Lean 4 establishing that no triple of consecutive powerful numbers exists below $10^{12}$ and below $10^{14}$, with the axiom footprint of both theorems being exactly {propext, Classical.choice, Quot.sound} -- no sorry, no native_decide, no trusted external computation. The statements are phrased in the byte-identical vocabulary of the google-deepmind/formal-conjectures formalization of the problem, and we prove abstractly that the open conjecture implies each bounded form, pinning the statement correspondence. The proof reduces the search to odd numbers via a mod-4 argument, represents every odd powerful number as $a^2 b^3$ with $a, b$ odd and $b$ squarefree, enumerates all odd powerful numbers by a fueled, kernel-reducible generator whose completeness is proved once and instantiated across 3,524 per-interval Boolean certificates, and eliminates the seven surviving distance-2 pairs (the members of OEIS A076445 below $10^{14}$) by explicit non-powerfulness witnesses. Every certificate's expected values are computed independently by a Python engine, so each kernel-checked equality doubles as a cross-implementation agreement. Total certified kernel time is roughly 46 CPU-hours. Larger uncertified computations exist (exhaustive to $10^{22}$; conditionally to about $7.38 \times 10^{28}$); our contribution is not a computational record but the elimination of trusted enumeration code from the evidence chain.