Collatz conjecture

Reference: Wikipedia

def collatzStep (n : ℕ) : ℕ

Consider the following operation on the natural numbers: If the number is even, divide it by two. If the number is odd, triple it and add one.

Equations

• collatzStep n = if Even n then n / 2 else 3 * n + 1

theorem CollatzConjecture (n : ℕ) (hn : n > 0) : ∃ (m : ℕ), collatzStep^[m] n = 1

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 Collatz conjecture states that for any positive integer $n$, there exists a natural number $m$ such that the $m$-th term of the sequence is 1.