Collatz conjecture for positive odd inputs

Open

CollatzMission.odd_inputs_conjecture

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

collatzdynamical-systemsnumber-theory

For every positive odd integer $n$ , there exists a nonnegative integer $m$ such that the $m$ -fold iterate of the classical Collatz map sends $n$ to $1$ .

Combined with the proved odd-input reduction, this statement implies the full Collatz conjecture.

Preamble

import Definitions.Def_CollatzMission

Formal statement

namespace CollatzMission

theorem odd_inputs_conjecture : OddInputsConjecture := by
  sorry

end CollatzMission

Source

https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Formulations.lean#L26-L28

View graph