---

Claim. Let $U$ be the set of odd positive integers not of the form $2^k+p$ with $p$ prime. Then $U$ is not the union of finitely many infinite arithmetic progressions and a set of asymptotic density zero. In particular $U$ is not one infinite arithmetic progression plus a density-zero set, so the question of Problem 16 has the answer no. The result is Chen, Y.-G., A conjecture of Erdős on $p+2^k$, arXiv:2312.04120 (v1 2023-12-07, v3 2024-02-18), the preprint link: in v3 the finitely-many form is Theorem 1.1 with Corollary 1.2, and the single-progression statement, that Erdős's conjecture (the paper's Conjecture A) is false, is Theorem 3.1, proved in Section 3; in v1 that single-progression statement is the paper's Theorem 1.1 and only theorem. Erdős's own 1950 covering-congruence construction, on the card erdos_1950_integers_form_related_problems (Theorem 3), is what puts an infinite progression inside $U$; Romanoff's theorem, Satz II on the card romanoff_1934_uber_einige_satze_der_additiven, is what gives the complement of $U$ in the odd numbers positive lower density. Chen's argument shows the progressions cannot absorb all but a null set of $U$.

Acceptance. The reviewed evidence is the documented acceptance by the catalog erdosproblems.com: its page for the problem (last edited 05 April 2026, the first discussion link) carries the label DISPROVED (LEAN) and its curator, Thomas Bloom, credits Chen's preprint with the negative answer. No refereed publication is recorded so the claim carries no refereed evidence; the acceptance rests on the catalog's curator and on the formal-conjectures catalog, which tags its statement erdos_16 as research solved with answer(False) and links the Lean proof below.

Formalization. Daniel Chin's ErdosProblem16 in Proofs/ErdosProblems/Erdos16.lean of https://github.com/danielchin/proofs, pinned above at the commit of 2026-02-25, is a link on this page because its author's announcement of the same day on the erdosproblems.com discussion thread (the second discussion link) presents it as a formalization of Chen's paper [Ch23], written with Gemini 3.1 Pro and Antigravity, the systems the author names there; the file itself has no header and names no author, source or system, and the formal-conjectures docstring instead credits the formalization to Chin using Aristotle, so this page follows the author's own statement. The file imports only Mathlib. It formalizes the second proof in Chen's paper, Theorem 3.1 with Lemmas 3.2--3.4 (Section 3, pp. 13--17 of v3; in v1 the same argument is Theorem 1.1 with Lemmas 2.1--2.3): with $U$ the odd integers not of the form $2^k+p$ for $k\ge1$, it states that there are no $m_0>0$, $a_0$ and set $W$ containing no infinite arithmetic progression (the file's density_zero) with $U=\{m_0h+a_0\}\cup W$. Its steps are Chen's: a progression $\{mh+a\}$ inside $U$ forces $m_0\mid m$ and $m_0\mid a-a_0$ (Lemma 3.2, the file's lemma1), the progressions $11184810s+992077$ and $11184810s+3292241$ lie in $U$ (Lemmas 3.3 and 3.4, firstap and secondap), and $\gcd(11184810,\,3292241-992077)=2$. The remainder condition is weakened from density zero to containing no infinite progression, so the file's theorem is stronger than Theorem 3.1, and since a set of density zero contains no infinite progression it implies the negative answer to the site's question. The file does not formalize Theorem 1.1 or Corollary 1.2 of v3, the finitely-many-progressions form, with which it is incomparable: that theorem allows finitely many progressions, the file allows a progression-free remainder of any density. This corpus has not built the file, printed its axioms or audited its definitions, so the claim carries no formalized evidence and the formalization is a link, not a warrant.

Depends on. Nothing in this wiki; the claim is Chen's preprint, which rests on Erdős's 1950 construction and Romanoff's theorem, cited through their library cards above.