Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of $\mathbb{Z}$ Has lcm Exceeding 10000
The Erdős-Selfridge odd covering problem (Erdős problem #7) asks whether a covering system of $\mathbb{Z}$ exists whose moduli are all odd, distinct, and greater than 1. The problem is open. We present a Lean 4 formalization, checked end to end by the proof kernel, of the exclusion: any covering of $\mathbb{Z}$ by finitely many congruence classes with distinct odd moduli > 1 has lcm of the moduli exceeding 10000. The proof composes a formalized density argument (a covering by divisors of $N$ exceeding 1 forces $2N \le σ_1(N)$, so the lcm is abundant or perfect), a kernel-checked abundancy…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2607.25628
curl -X POST /api/v1/records/arxiv/2607.25628/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.25628/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'