Erdős problem 456
Erdős [Er79e] writes it is 'easy to show' that for infinitely many we have .
Sources
FormalConjectures/ErdosProblems/
456.lean
Retained formal statement
It is trivial that always.
∀ (n : ℕ), Erdos456.m n ≤ Erdos456.p nTextbookStatement only, no proof