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