Erdős problem 1190

Let $\epsilon_m=\max \sum \frac{1}{n_i}$ where the maximum is taken over all finite sequences $m<n_1<\cdots<n_k$ for which there exist congruences $a_i\pmod{n_i}$ such that no integer satisfies two such congruences.

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1190.lean

Retained formal statement4 of 5

He could not even decide whether $\epsilon_m\to 0$ as $m\to \infty$ .

FormalConjectures/ErdosProblems/1190.leanErdos1190.erdos_1190.variants.tendsto_zero1 lineExact file

1Filter.Tendsto Erdos1190.eps Filter.atTop (nhds 0)

SolvedStatement only, no proof