Erdős Problem 422

Reference: erdosproblems.com/422

partial def Erdos422.f : ℕ+ → ℕ+

Let $f(1) = f(2) = 1$ and for $n > 2$ $$ f(n) = f(n - f(n - 1)) + f(n - f(n - 2)). $$

Note: It is not known whether $f(n)$ is well-defined for all $n$.

theorem Erdos422.erdos_422 : {n : ℕ+ | ∀ (x : ℕ+), f x ≠ n}.Infinite ↔ sorry

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

theorem Erdos422.erdos_422.variants.surjective : Function.Surjective f ↔ sorry

Is $f$ surjective?

theorem Erdos422.erdos_422.variants.growth_rate : (fun (n : ℕ+) => ↑↑(f n)) ≪ sorry

How does $f$ grow?

theorem Erdos422.erdos_422.variants.eventually_const : Filter.EventuallyConst f Filter.atTop ↔ sorry

Does $f$ become stationary at some point?