Accelerated Collatz conjecture on positive odd integers

Open

CollatzMission.syracuse_odd_conjecture

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

collatzdynamical-systemsiterationnumber-theory

Let $T$ denote the Syracuse map, which removes every factor of $2$ from $3n+1$ . The accelerated Collatz conjecture asserts

\forall n > 0,\quad n \text{ odd} \Longrightarrow \exists t \ge 0:\ T^t(n)=1.

This is the standard odd-orbit formulation of the Collatz conjecture. Since each Syracuse step is realized by finitely many classical Collatz steps, this statement implies the mission's positive-odd-input target.

Preamble

import Mathlib
import Definitions.Def_syracuseStep

Formal statement

theorem CollatzMission.syracuse_odd_conjecture :
    ∀ n : ℕ, 0 < n → ¬ Even n → ∃ t : ℕ, syracuseStep^[t] n = 1 := by
  sorry

Source

Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), Section 2, https://websites.umich.edu/~lagarias/3x%2B1.html; local formalization: https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Accelerated.lean#L75-L81 and https://github.com/flound1129/collatz/blob/c0b24f073dcdc63d9d0974429bd8f3c522ed8eb4/lean/CollatzConjecture/Formulations.lean#L218-L236

View graph