Formal target: Corpus.WikipediaJugglerConjecture.juggler_conjecture

Now form a sequence beginning with any positive integer, where each subsequent term is obtained by applying the operation defined above to the previous term.

Exact formal statement

∀ (n : Nat),
  GT.gt.{0} n 0 → Exists.{1} fun m => Eq.{1} (Nat.iterate.{1} Corpus.WikipediaJugglerConjecture.jugglerStep m n) 1

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record