The Collatz conjecture — 3n+1 is the only exactly critical map of its form
Start from a positive integer; halve it if even, triple it and add 1 if odd. Do you always reach 1? Unsolved since 1937. This article is the entrance to the four articles on the Collatz conjecture. It sets out the problem and where the world stands, and shows two things here — that 3n+1 is the only "exactly critical" map of this form (machine-checked) and the asymptotic of the stopping-time tail (paper). Criticality in full, the sign and the constant live in three deeper articles.
Leanmachine-checked (Lean 4 + mathlib, standard axioms only, no sorryAx, no native_decide; theorem names given)
paperproved, not yet machine-checked
computationchecked on this machine, within the range stated; not a claim made to the outside
knowna restatement, a known theorem, or a check of the literature
What the problem is
The Collatz conjecture: start from a positive integer n; if it is even, divide by 2; if it is odd, multiply by 3 and add 1. Repeat this. Do you always reach 1?
You can explain the problem to a schoolchild. And it has been unsolved since 1937. Erdős said that "mathematics is not yet ready for such problems."
The conjecture is made of two halves. That distinction runs through all four articles.
How far the world has come
| result | who / when | content |
|---|---|---|
| the distribution of v is known exactly | Terras 1976 | for odd n, setting v = v₂(3n+1), P(v=j) = 2⁻ʲ holds exactly (not approximately)known |
| almost every orbit comes down | Tao 2019 | for almost every n the orbit eventually falls below any arbitrarily slow function of n. It stops at "almost every"known |
| lower bound on cycle length | Eliahou 1993 | when verification stood at 2⁴⁰, the period of a nontrivial cycle is at least 17,087,915known |
| verification | reported as Barina 2025 | no counterexample up to 2⁷¹ |
| the neighbours are all broken | — | 3n−1 has three cycles, and 5n+1 diverges. Collatz is the sole survivor of this familyknown |
※ The verification record 2⁷¹ is as reported; the primary source has not been checked. The cycle lower bound (the criticality article) depends on that number.
What was done ① — 3n+1 is the only exactly critical map of this form
Place the Collatz map inside a wider family.
Divide out by p as far as it will go. Collatz is (p,q,r) = (2,3,1). Within this family, look for the multiplier that makes the expected ratio exactly 1.
Generalising Terras's theorem p-adically gives P(v=j) = (p−1)/pj, so—
When is this an integer? (p²−p−1) | (p²−1) ⟺ (p²−p−1) | p. But for p ≥ 3 we have p²−p−1 ≥ 5 > p, so it cannot divide.
It is an integer only for p = 2, and then qcrit = 3.
The Collatz map is the only "exactly critical" map of this form.
LeanShiori.qcrit_eq_three, Shiori.qcrit_not_int_of_three_le — the critical multiplier (p²−1)/(p²−p−1) is an integer only for p = 2, and then it is 3. The bundle and the ledger of axioms are in the Lean verification bundle.
Two faces of being critical
From P(v=j) = 2⁻ʲ we get E[2⁻ᵛ] = Σ4⁻ʲ = 1/3. Hence—
E[log ratio] = log(q/4) (negative for q < 4)
3 sits exactly on criticality in the ratio and on the safe side in the logarithm—it is alone at that point.
Once the +1 is included, E[nk+1 | nk] = nk + 1/3. The expectation keeps rising at every step.
Measured over 10 billion odd numbers and 34.9 billion steps, E[ratio] = 1.0000015. computation That the tail exponent is exactly 1 (Lagarias–Weiss 1992, ρRW = 1) and "E[ratio] = 1" are two ways of writing one claimknown. The three-line proof of uniqueness is elementary; it was not found in the literature searched, but it is the kind of statement that may well be known to specialists.
What was done ② — the stopping-time tail theorem
The stopping time of an odd n is the number of steps until the orbit first drops below its starting point. Let E(k) be the number of residue classes modulo 2k whose stopping time exceeds k (OEIS A076227), and set uk = E(k)/2k — the probability of not dropping below the starting point during k steps.
Notation: a = log₃2 = 0.6309297536, r = (1−a)/a = 0.5849625007, β = ln(1/r) = 0.5362075351, H = H₂(a) = 0.9499555272 (the binary entropy), ρ = 2−(1−H) = 0.9659065532, σ² = a(1−a), θk = ⌈ak⌉ − ak.
paper Here 𝓗 is the renewal function of the strict ascending ladder heights of the tilted walk (v equal to 1 with probability a). A is 1-periodic, with mean 10.892710 and relative amplitude βe−S = 7.59 %. Its Fourier coefficients also have a closed form — Â(m) = 1/(σ√(2π)(β − 2πim)(1 − χ̂(β − 2πim))), where χ̂ is the Laplace transform of the ascending ladder height.
The skeleton of the proof, and what is known
By Terras's bijection, uk is the probability that the i.i.d. walk Xi = vi − a (vi ∈ {0,1} uniform) stays positive for k steps. The mean is 1/2 − a = −0.1309, negative. The support of the step lies in (1−a) + ℤ, so the walk is neither lattice nor non-lattice but a non-centred lattice walk. The Cramér tilt (λ* = β, ψ(β) = ρ) moves it to a walk with zero drift and variance σ²; Theorem 6 of Vatutin–Wachtel 2009 (arXiv:0711.1302) — the conditioned local limit theorem for non-centred lattice walks — is applied with δk = k−1/4, and the part cut off is discarded by Σy>Y ry ≤ rY/(1−r). The constants close through the Sparre Andersen and Baxter–Spitzer identities.
known That the prefactor oscillates rather than converging on a non-centred lattice is stated in general by Vatutin–Wachtel 2009 (Theorems 1–2) and Mogulski–Rogozin 2005. What this theorem adds is the closed form (Â(m), the amplitude βe−S) and the application to A076227 — the Collatz stopping time.
computation E(1..24) agrees with A076227 by integer computation. A direct test of the VW local limit theorem at 41 points y ∈ (0,1) gives the ratio 0.99977 ± 0.00019. For k ∈ [2000, 12000] the residual yk − A(θk) lies on −456.8/k, with no constant offset. The Sparre Andersen identity holds in rationals for k ≤ 60.
This theorem does not touch the conjecture. However precise the asymptotic of uk, it excludes neither divergence nor cycles.
The three deeper articles
| article | what is there |
|---|---|
| Only 3n+1 is exactly critical | criticality in full; the overshoot distribution (an exact computation from the model agrees with a measurement over 10 billion odd numbers to 5 figures across 7 orders of magnitude); the boundary of exact counting (44 steps); the lower bound on cycle length (1.86×10¹¹ terms); and why the probabilistic argument is closed by the cycles of 3n−1 |
| What the sign of 1/3 decides | the sign decides which side of log₂3 a cycle approaches from, and not the size of the seat. In the binary-side model the sign of the asymmetry comes from 3³ < 2⁵, and the forbidden word DDD comes from the same inequality (Lean) |
| That constant is not yet a constant | the tail constant C of the overshoot ratio has a closed form, 0.4215205965; the value at each depth does not. The oscillation is a sawtooth indexed by the convergent denominators of log₂3, and the transfer operator has largest eigenvalue exactly 1/2 with no spectral gap |
What remains
Where the open items that have moved now stand is in What remains. Only what is open at present is placed here.
| content | |
|---|---|
| established | Collatz is the only exactly critical member of the family (qn+r)/pvLean |
| established | the stopping-time tail uk ρ−k k3/2 is asymptotic to a 1-periodic prefactor A(θk)paper |
| established | the overshoot distribution, the 44-step boundary, the cycle lower bound, the sign of the asymmetry, the closed form of C (the three articles) |
| not established | the conjecture itself. No result in the four articles proves or disproves it |
| not established | probabilistic arguments cannot tell 3n+1 from 3n−1; about cycles they can say nothing in principle |
| not established | the order of the error term in the tail theorem: the theorem gives o(1), the measurement O(1/k) (coefficient −457). The mean of the ascending ladder height, μ₁ = 0.2884300, has no closed form either. Lean not started |
Sources and reproduction
| item | kind | source / tool |
|---|---|---|
| P(v=j) = 2⁻ʲ | theorem | Terras (1976) |
| almost every orbit comes down | theorem | Tao (2019), arXiv:1909.03562 |
| the method for the cycle lower bound | theorem | Eliahou (1993) |
| verification to 2⁷¹ | as reported | Barina (2025). The primary source has not been read |
| tail exponent θ* = 1 | known | Lagarias–Weiss (1992), ρRW = 1 |
| uniqueness of qcrit(p) | machine-checked | Shiori.qcrit_eq_three, qcrit_not_int_of_three_le. The Lean verification bundle |
| the stopping-time tail theorem | paper | Vatutin–Wachtel, Probab. Theory Related Fields 143 (2009), arXiv:0711.1302, Theorem 6 / the Cramér tilt / Sparre Andersen / Baxter–Spitzer (Feller II §XII.7, §XVIII.3) |
| oscillating prefactor on a non-centred lattice | known | Vatutin–Wachtel 2009 Thms 1–2; Mogulski–Rogozin 2005. Doney arXiv:1006.5316 excludes this case |
| E(k) = A076227 | known | OEIS A076227 |
| E(1..24), the test of the local limit theorem, the residual −456.8/k | computed on this machine | integer DP, ⌈ak⌉ in 120-bit fixed point, FFT convolution |
| measurement over 10 billion odd numbers, 34.9 billion steps | computed on this machine | C, 4-way parallel |
Every tool used here is standard. Novelty is stated only as far as "not found in the literature searched" — the uniqueness of qcrit is elementary, the general form of the tail theorem is known, and what is added is the closed form and its application to this sequence.