---

Claim. Every finite covering system with pairwise distinct odd moduli greater than one has least common multiple greater than $10000$. This is the main theorem of I. Mian and S. Siddique, Kernel-Checked Exclusions for the Erdős–Selfridge Odd Covering Problem: Any Odd Covering of $\mathbb Z$ Has lcm Exceeding 10000, arXiv 2607.25628, posted 2026-07-28. The proof combines a density count, the reduction of possible periods to non-deficient odd integers, Chinese remainder capacity bounds for the $23$ odd non-deficient candidates below $10000$ and an enumeration showing that these are the only candidates; the library compiles the complete argument on its main theorem page. The authors describe the mathematical bound as known and their contribution as its formalization: the Lean 4 development pinned above, whose public CI run reports success with an axiom gate restricting the reported axioms to a subset of propext, Classical.choice and Quot.sound. The paper's acknowledgements say the development was carried out with the assistance of Claude (Anthropic).

Covers. The case of Problem 7 in which the period of the covering, the least common multiple of its moduli, is at most $10000$: no such distinct odd covering exists. The six-prime corollary on the page of Berger, Felzenbaum and Fraenkel already forces the period to be at least $255255$, so this exclusion is weaker than the refereed one. The unrestricted question stays open.

Depends on. Nothing in this wiki; the argument is the paper's own.

Standing. Claimed. There is no journal publication, the site's page for the problem does not cite the paper, and this corpus has not built or audited the Lean development, so the page lists no evidence; the public CI report is the authors' own. The library card records corrections to the paper's background references, which do not enter the finite exclusion.