Erdős problem 155

Is it true that for every $k \geq 1$ we have $F(N + k) \leq F(N) + 1$ for all sufficiently large $N$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

155.lean

Retained formal statement1 of 1

Is it true that for every $k \geq 1$ we have $F(N + k) \leq F(N) + 1$ for all sufficiently large $N$ ?

FormalConjectures/ErdosProblems/155.leanErdos155.erdos_1551 lineExact file

1True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1

OpenStatement only, no proof