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 statement6 of 7

Erdős [Er79e] writes it is 'easy to show' that $m_n/n \to \infty$ for almost all $n$ .

FormalConjectures/ErdosProblems/456.leanErdos456.erdos_456.variants.m_div_n3 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science