---

Claim. The statement of Problem 280 is false. Take $n_k=2^k$ for $k\ge1$, $a_1=0$ and $a_k=2^{k-1}+1$ for $k\ge2$. The growth condition holds with $\epsilon=1$, since $2^k>2k\log k$ for every $k\ge1$. For every $k\ge1$ the only $m$ with $0\le m<2^k$ in none of the classes $a_i\pmod{2^i}$, $1\le i\le k$, is $m=1$: an even $m$ lies in $0\pmod 2$, and an odd $m$ with $1<m<2^k$ has $m-1=2^{i-1}t$ with $t$ odd and $2\le i\le k$, so $m\equiv2^{i-1}+1\pmod{2^i}$. The count in the statement is therefore the constant $1$, which is $o(k)$. The site's commentary writes the system with $a_k=2^{k-1}+1$ for every $k\ge1$, the same classes since $2\equiv0\pmod2$. Cambie's comment of 2025-08-10 also records a second counterexample, which it attributes to Wouter van Doorn: a finite covering system with moduli $2,3,4,6,12$, which satisfy the growth condition for a small $\epsilon$, continued by any larger moduli, leaves nothing uncovered from $k=5$ on. A later comment of Cambie's (2025-08-11) notes what a nontrivial variant would need: with every $a_i=0$ at least $(1-o(1))\epsilon k$ primes below $n_k$ stay uncovered, so a counterexample needs moduli sharing prime factors with differing residues.

Submission note. Posted to the site's forum by Stijn Cambie on 10 August 2025:

This question can be answered in the negative, by e.g. the following two simple examples (and there should be more of course).

If one takes $n_i=2^i$ for every $i\ge 1$, $a_1=0,$ and $a_i=2^{i-1}+1$ for $i\ge 2$, then the desired number is actually $1$ (only the number $1$). The latter is $o(k)$.

As an alternative, Wouter van Doorn observed that $\{2,3,4,6,12\}$ (which can be extended to an infinite family) gives a covering with $n_i> i \log(i)$, also resolving the question.

Depends on. Nothing in this wiki.

Acceptance. Reviewed: the site's curator, Thomas Bloom, records the observation in the problem's commentary, credits Stijn Cambie in the page's acknowledgments and labels the problem disproved (page last edited 18 November 2025; the discussion thread's five comments date from 2025-08-10, 2025-08-11 and 2026-04-18, and the proof-claim tab was empty on 2026-10-07). Not refereed: the result is a forum comment with no write-up elsewhere; the construction is a few lines and is reproduced above in full.

Formalization. The site's label carries a Lean qualification. Lorenzo Luccioli posted on the thread (2026-04-18) a Lean formalization of the counterexample produced with Aristotle, at the pinned gist linked above. Boris Alexeev's lean-proofs repository holds a copy, src/latest/ErdosProblems/Erdos280.lean (added 2026-04-28; 262 lines at the pin of 2026-09-15), whose header names Cambie as informal author and Aristotle and Luccioli as formal authors. It proves Erdos280.not_erdos_280: there are sequences $n,a$ and $\epsilon>0$ with $n$ strictly increasing, $a_i<n_i$ for $i\ge1$, the growth condition for every $k\ge1$, exactly one uncovered $m<n_k$ for every $k\ge1$, and the uncovered count divided by $k$ tending to $0$; a comment in the file records the #print axioms output, propext, Classical.choice and Quot.sound, under the name Erdos280.erdos_280_counterexample, which the file's last line declares as an alias of not_erdos_280. The formal-conjectures statement file, at the commit of 2026-09-18 linked from the problem page, carries the category research solved and a formal_proof attribute pointing to the repository's v4.29.1 copy on its main branch, unpinned; its erdos_280 states the problem under answer(False) with uncoveredCount over Finset.range (n k) and indices $1\le i\le k$. This corpus has not built or audited either development, so the page lists no formalized evidence.