Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

The Syracuse map takes odd values

Proved
syracuseStep_odd

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

dynamical-systemsiterationnumber-theorystopping-time

Let T(n)=(3n+1)/2 v2(3n+1)T(n) = (3n+1)/2^{\,v_2(3n+1)}T(n)=(3n+1)/2v2​(3n+1) be the Syracuse map. Then T(n)T(n)T(n) is odd for every nnn:

T(n) is odd.T(n) \text{ is odd} .T(n) is odd.

By construction T(n)T(n)T(n) is the odd part of 3n+13n+13n+1, that is, the quotient of 3n+13n+13n+1 by the largest power of 222 dividing it, so no factor of 222 survives. Since 3n+1≠03n+1 \ne 03n+1=0 for every natural nnn, the statement needs no hypothesis.

The fact is what makes the Syracuse map a self-map of the odd numbers, and hence what allows its iterates to be formed and compared with the Collatz orbit.

Preamble
import Mathlib
import Definitions.Def_syracuseStep
Formal statement
theorem syracuseStep_odd (n : ℕ) : Odd (syracuseStep n) := by
  sorry
Source
https://en.wikipedia.org/wiki/Collatz_conjecture; supporting lemma for the prove2.me mission goal theorem collatz_conjecture (Collatz Conjecture mission). Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), 3-23, Section 2 (the function T and its relation to the Collatz map), https://websites.umich.edu/~lagarias/3x%2B1.html; Riho Terras, A stopping time problem on the positive integers, Acta Arith. 30 (1976), 241-252.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me