Erdős problem 202

Let $n_1<\cdots < n_r\leq N$ with associated $a_i\pmod{n_i}$ such that the congruence classes are disjoint (that is, every integer is $\equiv a_i\pmod{n_i}$ for at most one $1\leq i\leq r$ ). How large can $r$ be in terms of $N$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

202.lean

Retained formal statement2 of 2

Erdős and Stein conjectured that $f(N)=o(N)$ , which was proved by Erdős and Szemerédi [ErSz68].

FormalConjectures/ErdosProblems/202.leanErdos202.erdos_202.variants.erdos_szemeredi1 lineExact file

1(fun N => ↑(Erdos202.f N)) =o[Filter.atTop] fun N => ↑N

SolvedStatement only, no proof