---

Claim. The answer to Problem 281 is yes. Let $n_1<n_2<\cdots$ be positive integers such that for every choice of residues $a_i\pmod{n_i}$ the integers lying in none of the classes have density $0$. Then for every $\epsilon>0$ there is a $k$ such that, for every choice of residues, the integers lying in none of the first $k$ classes have density below $\epsilon$. The argument identifies a residue choice $a=(a_i)$ with a point of the compact product of the groups $\mathbb Z/n_i\mathbb Z$ and works in the profinite integers $\widehat{\mathbb Z}$ with their Haar probability measure $\mu$. For each $k$ the set $C_k(a)$ of profinite integers avoiding the first $k$ classes is clopen and periodic modulo $\operatorname{lcm}(n_1,\ldots,n_k)$, and $\mu(C_k(a))$ equals the density $d_k(a)$ of the integers avoiding those classes; the sets decrease to $C(a)=\bigcap_kC_k(a)$, so $d_k(a)\to\mu(C(a))$. If $\mu(C(a))>0$ for some $a$, translation invariance and an averaging argument (the pointwise ergodic theorem for the shift, or Fatou's lemma applied to the complements) give a shift $x$ for which $(C(a)-x)\cap\mathbb Z$ has positive upper density; but $C(a)-x=C(a')$ for the shifted residue choice $a'$, against the hypothesis. So $d_k(a)\to0$ for every $a$. Each $d_k$ depends only on the first $k$ coordinates, so it is continuous on the compact space of choices, and the sequence decreases pointwise to $0$; Dini's theorem makes the convergence uniform, which is the claim. As a reviewer on the thread noted, the ergodic form of the argument proves more: it needs only that the integers avoiding every class have lower density $0$, while the Fatou form controls only the upper density of the avoiding set, which the problem's hypothesis still supplies.

Neel Somani posted the argument on 2026-01-17 as produced with GPT-5.2 Pro, linking the transcript; the site's commentary credits the proof to Somani using ChatGPT. The fuller write-up linked above was posted on the thread the same day by Nat Sothanaphan after Sothanaphan's assessment, prepared with ChatGPT.

Submission note. Posted to the site's forum by Neel Somani on 17 January 2026:

I generated this proposed solution using GPT 5.2 Pro. Sharing here for verification: https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e0816e

Here is a short summary:

Work in the profinite integers $\widehat{\mathbb Z}$ with Haar measure, where "avoid the first k congruences" is a clopen set whose Haar measure equals the usual asymptotic density of avoiding integers. These measures decrease with k to the Haar measure of the infinite intersection. If that limiting measure were greater than 0 for some residue choice, then translation invariance + averaging (Fatou) gives a shift x so that the shifted set corresponds to another residue choice and contains integers of positive upper density, contradicting the hypothesis that every residue choice leaves density 0 uncovered. Hence the limit is always 0, and since the finite‑k densities vary continuously over the compact space of residue choices, Dini/compactness upgrades pointwise $\to$ uniform, giving a single $k(\varepsilon)$.

If there's a gap, I suspect it's in the step $\mu(C)>0\Rightarrow\exists x$ with $(C-x)\cap\mathbb N$ having positive upper density (and in identifying that translate with an admissible residue choice).

Depends on. Nothing in this wiki. An independent elementary proof from two classical theorems is recorded on its own claim page.

Acceptance. Reviewed: the site's curator, Thomas Bloom, credits the proof in the problem's commentary and labels the problem proved (page last edited 18 January 2026; the thread had 28 comments and an empty proof-claim tab on 2026-10-07). On the thread, Bloom wrote on 2026-01-17 that the argument looked right to Bloom and singled out the passage to the profinite completion; Terence Tao assessed it the same day, recast it as a combinatorial argument with the Hardy-Littlewood maximal inequality in place of the ergodic theorem, and on 2026-01-18 settled a dispute over the Fatou step in the argument's favor; Nat Sothanaphan assessed it as correct with some details omitted and produced the fuller write-up. Not refereed: there is no journal or preprint publication.

Formalization. The site's label carries a Lean qualification. JakeMallen posted on the thread (2026-01-19, the post linked above) a Lean formalization of the argument produced with Aristotle and Gemini 3.0 Flash, the posting the site's qualification rests on. Boris Alexeev's lean-proofs repository holds src/latest/ErdosProblems/Erdos281.lean (added 2026-04-29; 1,195 lines at the pin of 2026-09-15), whose header names Neel Somani and GPT-5.2 Pro as informal authors and Aristotle, Gemini 3.0 Flash and JakeMallen as formal authors. It proves Erdos281.erdos_281: for strictly increasing positive $n$, Erdos281Hyp (every residue choice has avoidAll of two-sided density $0$, with densities over $[-N,N]$) implies Erdos281Concl (for every $\epsilon>0$ some $k$ such that every choice has avoidPrefix of some density $d<\epsilon$), through Haar measure on a profinite-integer type; a comment records the #print axioms output, propext, choice and Quot.sound, under the name Erdos281.Erdos_281, which the file's last line declares as an alias of erdos_281. The formal-conjectures statement file, at the commit of 2026-09-18 linked from the problem page, carries the category research solved, says the linked proof formalizes Somani's argument, and points to the repository's v4.29.1 copy on its main branch, unpinned; its erdos_281 uses Set.HasIntDensity with the same shape under answer(True). This corpus has not built or audited either development, so the page lists no formalized evidence.