Wikipedia · research open · AMS 11 37
unsolvedsorry — nobody on it
Juggler conjecture
Conjecture · 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. The **Juggler Conjecture** states that for any positive integer , there exists a natural number such that the -th term of the sequence is .
Formal statement · Lean 4.lean
theorem juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ m, jugglerStep^[m] n = 1 := by
sorryProof. sorry
Nobody has tried yet.