Erdős problem 688 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

688.lean

Retained formal statement4 of 4

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}$ .

FormalConjectures/ErdosProblems/688.leanErdos688.erdos_688.variants.lglglg_over_lglg_is_big_o1 lineExact file

1(fun n => Real.log (Real.log (Real.log ↑n)) / Real.log (Real.log ↑n)) =O[Filter.atTop] Erdos688.epsilonFunction

SolvedStatement only, no proof