Erdős problem 456 · problems.science

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

Sources

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

456.lean

Retained formal statement2 of 7

Does $p_n/m_n \to \infty$ for almost all $n$ ?

FormalConjectures/ErdosProblems/456.leanErdos456.erdos_456.parts.ii4 linesExact file

1True ↔2  ∃ A,3    Filter.Tendsto (fun N => ↑(Nat.count A N) / ↑N) Filter.atTop (nhds 1) ∧4      Filter.Tendsto (fun n => ↑(Erdos456.p n) / ↑(Erdos456.m n)) (Filter.atTop ⊓ Filter.principal A) Filter.atTop

OpenStatement only, no proof

Sources

Search problems.science