---

Claim. The answer to Problem 26 is no, by a set with divergent reciprocal sum. The proof is a Lean 4 development by the DeepMind prover agent in a fork of formal-conjectures, posted to the site's thread by GTsoukalas on 2026-04-06 with an informal write-up and merged into formal-conjectures the same day as the solution of erdos_26.variants.tenenbaum, whose docstring there says that the DeepMind prover agent found the formal disproof.

The construction. Fix an increasing sequence of primes $q_0<q_1<\cdots$ with $q_0\geq 29$. The set is built in blocks. Block $m$ consists of the numbers $R_m+jP_m$ for $1\leq j\leq L_m$, where $J_m$ is the number of terms before the block, $P_m$ is divisible by $q_k$ for every $k\leq 10J_m$, $R_m$ is chosen by the Chinese remainder theorem so that $q_k$ divides $R_m+k$ for the same $k$, and $L_m$ is chosen so that the block's reciprocal sum lies between $1/10$ and $2/10$. The reciprocal sum of the whole set therefore diverges, and for a shift $k$ every term $a$ of a block with $10J_m\geq k$ has $q_k\mid a+k$, so from some block on every shifted term is a multiple of the prime $q_k$.

What the file proves. elementary_thick_sequence_exists gives a strictly increasing $A:\mathbb{N}\to\mathbb{N}$ with divergent reciprocal sum such that for every $k$ the set of multiples of $A+k$ has lower density at most $1/2$; counterexample_exists derives from it that no shift $A+k$ is weakly Behrend with $\varepsilon=1/4$; and erdos_26.variants.tenenbaum concludes that Tenenbaum's variant, that for every $\varepsilon>0$ some shift makes the multiples of $A+k$ reach lower density at least $1-\varepsilon$, is false. The thread's write-up and the site's commentary state the stronger bound that the multiples of every $A+k$ have upper density below $0.34$, which the file does not state. One further step, which the file does not state either, settles the problem: a set of multiples of density one has lower density one, so no $A+k$ is Behrend, and the answer to the question is no for this thick set. The same set refutes the formal-conjectures statement erdos_26, which restricts the question to sequences with divergent reciprocal sum and which the formalization of Ruzsa's construction on Ruzsa's claim page does not prove.

Acceptance. None. This corpus has not built or audited the file, so no formalized evidence is listed. The site's curator credits DeepMind for the negative answer to Tenenbaum's variant only, and the site's label rests on the earlier claims of Davenport and Erdős and Ruzsa, so nothing is reviewed; nothing is refereed.

Depends on. Nothing in this wiki.