Erdős problem 422

Does $f(n)$ miss infinitely many integers?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

422.lean

Retained formal statement2 of 4

Does $f$ become stationary at some point?

FormalConjectures/ErdosProblems/422.leanErdos422.erdos_422.variants.eventually_const1 lineExact file

1True ↔ Filter.EventuallyConst Erdos422.f Filter.atTop

OpenStatement only, no proof