Back to Problems
erdos_409.parts.i.variants.isLittleO
Specification
Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = o(g(n))$?
Lean 4 Statement
theorem erdos_409.parts.i.variants.isLittleO (c : ℕ → ℕ)
(h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
(fun n => (c n : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ)
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.