Erdős problem 85
Is it true that, for all large , ?
Sources
FormalConjectures/ErdosProblems/
85.lean
Retained formal statement
Is it true that, for all large , ?
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos85.f n ≤ Erdos85.f (n + 1)OpenStatement only, no proof