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
If we allow for then Rusza has found a counter-example.
∃ A, StrictMono A ∧ ¬Erdos26.IsThick A ∧ ∀ (k : ℕ), ¬Erdos26.IsBehrend fun x => A x + kSolvedStatement only, no proof