Erdős problem 1101

Does there exist a good pairwise-coprime sequence $u_n$ with $\sum 1/u_n < \infty$ and polynomial growth? What if one only requires $u_n \le e^{o(n)}$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1101.lean

Retained formal statement2 of 2

2. There is a good sequence with sub-exponential growth.

FormalConjectures/ErdosProblems/1101.leanErdos1101.erdos_1101.parts.ii1 lineExact file

1∃ u, Erdos1101.IsGood u ∧ (fun n => Real.log ↑(u n)) =o[Filter.atTop] fun n => ↑n

OpenStatement only, no proof