Skip to content

Erdős problem 688

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

688.lean

Retained formal statement3 of 4

In particular, is it true that ϵn=o(1)\epsilon_n = o(1)?

FormalConjectures/ErdosProblems/688.leanErdos688.erdos_688.parts.ii1 lineExact file
True ↔ Erdos688.epsilonFunction =o[Filter.atTop] fun n => 1
OpenStatement only, no proof