A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below 1014
Abstract
Erdős problem 364 asks whether three consecutive powerful numbers exist, where n is powerful if p | n implies p2 | 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 1012 and below 1014, 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 a2 b3 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 1014) 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 1022; conditionally to about 7.38 × 1028); our contribution is not a computational record but the elimination of trusted enumeration code from the evidence chain.
Related
- Towards the Erdős matching conjecture for 4‐uniform hypergraphs: Stability and applications
- The Erdős--Chvátal Simplex Conjecture
- A counterexample to the Erdős--Sós bipartite-link conjecture
- Erdős--Straus Conjecture: Modular Inversion in Mordell Classes
- A proof of the Erdős-Gallai cycle decomposition conjecture
BibTeX
@misc{mian2026kernelcertified,
title = {{A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below $10^14$}},
author = {Ibrahim Mian and Shayaan Siddique},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.25011},
eprint = {2609.25011},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.25011},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below 10^14
AU - Ibrahim Mian
AU - Shayaan Siddique
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.25011
UR - https://arxiv.org/abs/2609.25011
AB - Erdős problem 364 asks whether three consecutive powerful numbers exist, where n is powerful if p | n implies p^2 | 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 × 10^28); our contribution is not a computational record but the elimination of trusted enumeration code from the evidence chain.
ER -