Erdős problem 26
Let be infinite. Must there exist some such that almost all integers have a divisor of the form for some ? The question as posed follows negatively from Davenport–Erdős (1951). The AI result settles Tenenbaum's harder variant, also negatively: there is an infinite such that for every the set of multiples of has upper density below .
Sources
FormalConjectures/ErdosProblems/
26.lean
Retained formal statement
∀ {ι : Type u_1} (A : ι → ℕ) {ε : ℝ}, ε < 0 → ¬Erdos26.IsWeaklyBehrend A εTestStatement only, no proof