Erdős problem 456

Erdős [Er79e] writes it is 'easy to show' that for infinitely many $n$ we have $m_n < p_n$ .

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

456.lean

Retained formal statement5 of 7

Linnik's theorem implies that $p_n\leq n^{O(1)}$ .

FormalConjectures/ErdosProblems/456.leanErdos456.erdos_456.variants.linniks_theorem1 lineExact file

1∃ L, (fun n => ↑(Erdos456.p n)) =O[Filter.atTop] fun n => ↑n ^ L

SolvedStatement only, no proof