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 nn, there exists a natural number mm such that the mm-th term of the sequence is 11.

Formal statement · Lean 4.lean
theorem juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ m, jugglerStep^[m] n = 1 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗