Erdős problem 1135

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.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

1135.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/1135.leanErdos1135.erdos_11351 lineExact file

1∀ n > 0, ∃ m, CollatzConjecture.collatzStep^[m] n = 1

OpenStatement only, no proof