theorem Collatz.collatz_conjecture (n : ℕ) : 1 ≤ n → CollatzConverges n

The Collatz conjecture: every positive integer eventually reaches 1.

theorem Collatz.collatz_unique_cycle (k n : ℕ) : 1 ≤ n → Function.IsPeriodicPt collatz k n → k > 0 → n = 1 ∨ n = 2 ∨ n = 4

There are no non-trivial cycles: the only cycle reachable from positive integers is {1, 4, 2}.