Motivation and history

The Collatz conjecture, also called the $3x+1$ problem, asks whether one elementary iteration rule has the same long-term behavior for every positive integer. It belongs to number theory and discrete dynamical systems: the rule is deterministic and trivial to compute for any fixed input, but no argument is known that controls every orbit. The problem has served as a test case for methods involving congruences, stopping times, probabilistic models, computation, and arithmetic dynamics. Jeffrey Lagarias's survey, The $3x+1$ Problem and Its Generalizations, organized much of the classical theory and explains why strong results about large classes of starting values do not settle the universal statement (Lagarias 1985).

The problem has a long record of partial results. By 1985, the literature already included results on stopping-time densities, possible cycles, and divergent trajectories, summarized by Lagarias. In 2019, Terence Tao proved that for every function $f(N)$ tending to infinity, the minimum value attained by the orbit of $N$ is at most $f(N)$ for almost all positive integers $N$, where “almost all” is measured using logarithmic density (Tao 2019). This is a strong statement about typical orbits, but it does not cover every starting value. Computational verification has also been pushed to very large finite ranges; David Barina describes algorithms and verification methods for this task in Convergence Verification of the Collatz Problem (Barina 2021). A finite verification bound, regardless of size, leaves all larger starting values outside its scope.

Setting

For a natural number $n$, define the Collatz step $C(n)$ by

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

Write $C^m(n)$ for the result of applying $C$ exactly $m$ times, with $C^0(n)=n$. The forward orbit of $n$ is therefore

$$n,\ C(n),\ C^2(n),\ C^3(n),\ldots.$$

The familiar orbit beginning at $6$, for example, starts $6,3,10,5,16,8,4,2,1$. Reaching $1$ is the relevant event; after that point the usual map continues around the cycle $1,4,2,1$.

Formalization target

The mission goal is the universal assertion

$$\forall n\in\mathbb N,\quad n>0\Longrightarrow \exists m\in\mathbb N,\quad C^m(n)=1.$$

The existential index $m$ may be zero, so the case $n=1$ is included directly. The hypothesis $n>0$ excludes $0$, whose behavior under the total natural-number definition of $C$ is irrelevant to the conjecture.

The goal is the existing public prove2.me theorem collatz_conjecture, rather than a new copy. Its statement follows the Collatz declaration in the Formal Conjectures collection.

Significance

A proof would classify every positive-integer orbit with respect to reaching $1$. It would simultaneously rule out an orbit that escapes forever without visiting $1$ and any nontrivial cycle disjoint from $1$. Partial density results and finite computations establish neither universal exclusion.

The formalization goal is to make the universal quantifiers, parity split, finite iteration, and boundary cases explicit in Lean 4. Supporting contributions can isolate reusable facts about iterates, stopping times, accelerated odd-only maps, residue classes, and finite certificates. Such components may also support formal work on related piecewise-affine integer dynamical systems, while every contribution remains tied to a precisely stated theorem.

Difficulty

Individual trajectories can be computed, and many families of inputs can be reduced by elementary parity arguments, but the map combines contraction and expansion. Even steps halve the current value, while odd steps replace it by the larger value $3n+1$. Local information about a bounded initial segment of an orbit does not supply a uniform bound on all later values or on the time required to reach $1$.

Statistical control of most inputs also leaves exceptional inputs unresolved. Likewise, excluding cycles up to a finite length does not exclude longer cycles, and checking all inputs below a finite threshold does not constrain every larger input. The mission therefore requires statements whose quantifiers genuinely cover all positive natural numbers; a large finite computation or an almost-everywhere theorem cannot by itself close the goal.

Formalization scope

The existing Lean statement works over ℕ. Its local collatzStep definition branches on the proposition that $n$ is even, uses natural-number division by $2$ on the even branch, and uses $3n+1$ on the odd branch. Iteration is represented by the standard finite function iterate notation. The theorem quantifies over a positive starting value $n$ and asserts the existence of a finite iterate index $m$ at which the value is exactly $1$.

The positivity hypothesis is essential: the total function sends $0$ to $0$, so including $0$ would make the universal statement false. The mission does not replace the universal quantifier by a fixed numerical bound, and it does not encode a predetermined stopping-time limit. A complete solution must account for every positive starting value.

Useful supporting formalizations include exact relations between the classical and accelerated maps, composition laws for finite iteration, stopping-time predicates, cycle exclusion statements, descent criteria, and checked finite ranges. Each supporting theorem should state its own hypotheses and trust boundary explicitly. Computational artifacts are welcome when their finite scope is stated precisely and their result is connected to a Lean consumer through a checked certificate or another accepted verification boundary.

Selected references

• Jeffrey C. Lagarias, The $3x+1$ Problem and Its Generalizations, American Mathematical Monthly 92 (1985), 3–23. https://websites.umich.edu/~lagarias/3x%2B1.html
• Terence Tao, Almost All Orbits of the Collatz Map Attain Almost Bounded Values, 2019; published in Forum of Mathematics, Pi 10 (2022). https://arxiv.org/abs/1909.03562
• David Barina, Convergence Verification of the Collatz Problem, The Journal of Supercomputing 77 (2021), 2681–2688. https://doi.org/10.1007/s11227-020-03368-x
• Google DeepMind, Formal Conjectures: Collatz Conjecture, Lean 4 statement. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean