---

Claim. The answer to Problem 26 is no, by an explicit set. Let $p_j$ be the $j$th prime and choose $n_1<n_2<\cdots$ with $n_l\equiv-(j-1)\pmod{p_j}$ for every $j\leq l$, which the Chinese remainder theorem allows. Ruzsa's set is $A=\{n_1,n_2,\ldots\}$. For a shift $k\geq 1$, every $n_l+k$ with $l>k$ is divisible by $p_{k+1}$, so an integer congruent to one modulo $p_{k+1}\prod_{l\leq k}(n_l+k)$ has no divisor in $A+k$; these integers form an arithmetic progression of positive density, so $A+k$ is not a set of multiples of density one for any $k$. This is the mechanism the formalization below proves: for each $k$ an arithmetic progression disjoint from the multiples of $A+k$.

Context. The construction is reported on the site's problem page, which credits it to Ruzsa; Ruzsa did not publish it himself, and Erdős reported its existence, without the construction, in [Er95] (Erdős 1995). The admissible $n_l$ form a residue class modulo $p_1\cdots p_l$, so the terms may be chosen to grow like the primorials; the reciprocal sum then converges and the negative answer also follows from the Davenport--Erdős theorem on the claim page Davenport and Erdős. The site's commentary adds that van Doorn modified the construction to give a counterexample whose reciprocal sum diverges, which answers the question in the negative for thick sets too; the thread discussed that modification on 2025-11-24.

Formalization. The linked Lean file in Boris Alexeev's repository declares itself a formalization of Ruzsa's counterexample, auto-formalized by Aristotle (Harmonic); its header reports the proof verified by Lean 4.24.0 with the matching Mathlib. It proves two theorems. Its own statement, ruzsa_counterexample, is the construction above: an infinite set $A$ such that for every $k\geq 1$ the integers with no divisor in $A+k$ have positive lower density. The formal-conjectures project's erdos_26.variants.rusza, an infinite strictly increasing sequence with convergent reciprocal sum none of whose shifts is Behrend, it proves instead with the witness $2^{2^n}$, bounding the upper density of the multiples of the shifted sequence by $\sum_i 1/(2^{2^i}+k)<1$; that is the convergent-sum route of the Davenport--Erdős page, not Ruzsa's set. The file does not prove the project's main statement erdos_26, which restricts the question to sequences with divergent reciprocal sum, although that declaration's formal_proof attribute names the file. The link is pinned to the last commit that touched the file at that path, and the file was announced in the site's thread on 2025-12-28, the day the community database records the site's status as disproved. This corpus has not built or audited the file, so the page lists no formalized evidence.

Acceptance. The site's curator, T. F. Bloom, marks the problem disproved and presents Ruzsa's construction as the counterexample, which the page lists as reviewed. Nothing is refereed. Erdős reported the counterexample in [Er95] (Resenhas IME-USP 2 (1995), no. 2, 165--186; p. 167 as the site cites it; item 4 of Part I, p. 3 of the author's typescript). Right after stating the question as one he and Tenenbaum had recently asked, he wrote that "Very recently Ruzsa found a very ingenious counterexample", without giving it, and added Tenenbaum's $\varepsilon$-variant. The construction above is the one the site credits to Ruzsa. That report dates this page. Its record gives no month, so the first day of 1995 stands in for the issue date. The formalization was announced in the site's thread on 2025-12-28, the formalization link's own date.