Problem 254

Let $A\subseteq \mathbb{N}$ be such that

\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty

and

\sum_{n\in A} \{ \theta n\}=\infty

for every $\theta\in (0,1)$ , where $\{x\}$ is the distance of $x$ from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of $A$ .

Source: erdosproblems.com/254

Number theory

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

OPEN, the site's label (page last edited 7 December 2025). The corpus accepts Fan's full proof claim of July 2026 on formalized evidence (claim page (Fan, 2026)): Boris Alexeev's Lean formalization of the preprint's six-per-interval version, with OpenAI Codex as its formal author, was built here and its theorem audited against the Statement above, so the problem stands solved and proved; the preprint's Corollary 1.2, at five elements in every large dyadic interval, is not built. Snyder's Lean proof of the statement as posed (claim page (Snyder, 2026)), which formal-conjectures registers as the formal proof of its statement, is pending; the corpus has not built or audited it. The site has not accepted either claim, and neither has a refereed version or independent review.

Problem 254

Status

Proof claims

Discussion