Prove2Me

Collatz step map C(n)C(n)

Definition
collatzStepMap

by Zexuan Liu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemsiterationnumber-theory

The Collatz step map on the natural numbers,

C(n)={n/2,n even,3n+1,n odd.C(n) = \begin{cases} n/2, & n \text{ even},\\ 3n+1, & n \text{ odd}.\end{cases}

The even branch uses natural-number division, so the function is total on N\mathbb{N}; in particular C(0)=0C(0)=0, which is why every statement about the Collatz dynamics carries a positivity hypothesis on the starting value. The Lean declaration is collatzStep, character-for-character the definition appearing in the preamble of the mission goal theorem collatz_conjecture, packaged here as an importable module so that supporting lemmas and the goal statement share a single Lean constant.

Definition code
import Mathlib.Algebra.Group.Nat.Even

/-- One step of the Collatz map: an even number is halved, an odd number `n` is sent to
`3 * n + 1`.  Natural-number division is used on the even branch, so the definition is total;
`collatzStep 0 = 0`. -/
def collatzStep (n : ℕ) : ℕ :=
  if Even n then n / 2 else 3 * n + 1
Source
https://en.wikipedia.org/wiki/Collatz_conjecture; matches the local definition in the preamble of the prove2.me theorem collatz_conjecture, itself following google-deepmind/formal-conjectures, FormalConjectures/Wikipedia/CollatzConjecture.lean: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean

View graph