A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below $10^{14}$
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.25011
curl -X POST /api/v1/records/arxiv/2609.25011/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.25011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'