Erdős problem 688

Erdős claims in [Er80] (p. 106) that it is not difficult to prove $\epsilon_n \gg \frac{\log\log\log n}{\log\log n}$ .

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

688.lean

Retained formal statement2 of 4

Estimate $\epsilon_n$ - upper bound.

FormalConjectures/ErdosProblems/688.leanErdos688.erdos_688.parts.i.upper_bound1 lineExact file

1Erdos688.epsilonFunction =O[Filter.atTop] sorry

OpenStatement only, no proof