Claims

../

1951_01_01_davenport_erdos: Davenport and Erdős showed that the multiples of a sequence with convergent reciprocal sum have a density, the limit over its finite stages; that limit is below one, so every shift of such a set fails; the site credits this.

1995_01_01_ruzsa: An explicit infinite sequence, built by the Chinese remainder theorem, each of whose shifted copies misses the divisors of a whole arithmetic progression; reported by Erdős in 1995 and formalized in Lean by others.

2026_04_06_deepmind: A Lean proof by the DeepMind prover agent of an increasing sequence with divergent reciprocal sum none of whose shifts has multiples of lower density above one half; it refutes Tenenbaum's variant and the question.

---