Erdős Problem 1135

References:

• erdosproblems.com/1135
• [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
• [La10] Lagarias, Jeffrey C., The {$3x+1$} problem: an overview. (2010), 3--29.
• [La16] Lagarias, Jeffrey C., Erd\H os, {K}larner, and the {$3x+1$} problem. Amer. Math. Monthly (2016), 753--776.
• [La85] Lagarias, Jeffrey C., The {$3x+1$} problem and its generalizations. Amer. Math. Monthly (1985), 3--23.

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.

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

Alias of CollatzConjecture.collatzConjecture.

---

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.