Reduction to positive odd inputs

Proved

CollatzMission.collatz_of_odd_inputs

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

collatzdynamical-systemsnumber-theory

Let $T(n)=n/2$ when $n$ is even and $T(n)=3n+1$ when $n$ is odd. Assume every positive odd integer reaches $1$ after finitely many iterations of $T$ . Then every positive integer reaches $1$ after finitely many iterations.

This reduction removes powers of two by strong induction and isolates the odd-input form of the Collatz conjecture.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

theorem collatz_of_odd_inputs :
    OddInputsConjecture → ∀ n : ℕ, 0 < n → ∃ m : ℕ, collatzStep^[m] n = 1 := by
  sorry

end CollatzMission

Source

https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Formulations.lean#L43-L80

View graph