Erdős problem 1135
The Collatz conjecture states that for any positive integer , there exists a natural number such that the -th term of the sequence is 1.
Sources
FormalConjectures/ErdosProblems/
1135.lean
Retained formal statement
The Collatz conjecture states that for any positive integer , there exists a natural number such that the -th term of the sequence is 1.
∀ n > 0, ∃ m, CollatzConjecture.collatzStep^[m] n = 1OpenStatement only, no proof