{"id":"arxiv/2609.25011","url":"https://arxiv.org/abs/2609.25011","tags":["math.GM","cs.LO"],"score":0,"title":"A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below $10^{14}$","domain":"math.GM","source":"arxiv","authors":["Ibrahim Mian","Shayaan Siddique"],"reviews":0,"subject":"math.GM","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-29","reactions":{}}