Formal target: Corpus.WikipediaCollatzConjecture.collatz_conjecture

For a positive integer n, define C(n) = n/2 when n is even and C(n) = 3n + 1 when n is odd. Starting from n, repeatedly apply C. Is it true that for every n ≥ 1 there is an integer m ≥ 0 for which C iterated m times sends n to 1? The starting value counts as the zeroth iterate; negative integers and zero are not part of the question.

Exact formal statement

∀ (n : Nat),
  GT.gt.{0} n 0 → Exists.{1} fun m => Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep m n) 1

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record