Formal target: Corpus.OEIS87207.conjecture

Starting at any $n$ and iterating the map $n \mapsto a(n)$, we will always reach $0$.

Exact formal statement

∀ (n : Nat), Exists.{1} fun k => Eq.{1} (Nat.iterate.{1} Corpus.OEIS87207.a k n) 0

This target is a formal statement, not a proof of the problem.

Environment availability: available.