What is the conjecture
https://www.erdosproblems.com/25
Let $n_1<n_2<\cdots$ be an arbitrary sequence of integers, each with an associated residue class $a_i\pmod{n_i}$. Let $A$ be the set of integers $n$ such that for every $i$ either $n<n_i$ or $n\not\equiv a_i\pmod{n_i}$. Must the logarithmic density of $A$ exist?
Status: open
Prerequisites needed
logarithmic density could be put into ForMathlib, since other problems also use it.
also see #201
Choose either option