number-theory · dynamical-systems · integer-iteration
For a positive integer n, define C(n) = n/2 when n is even and C(n) = 3n + 1 when n is odd. Starting from n, repeatedly apply C. Is it true that for every n ≥ 1 there is an integer m ≥ 0 for which C iterated m times sends n to 1? The starting value counts as the zeroth iterate; negative integers and zero are not part of the question.
Why it matters
One elementary rule produces trajectories that can grow before falling. The challenge is a statement about every starting integer, not just a large finite search or almost every integer.
One possible first attack
Prove that every starting value 2^r reaches 1 after r steps, then prove a trajectory-composition lemma: a start that reaches a previously settled start also reaches 1. These are reusable elementary lemmas, not a proposed solution of the general conjecture.
Mathematical status
Open, checked 2026-09-11 against Erdős Problem 1135 and Tao’s primary paper. Tao proves that almost all orbits attain values below any prescribed function tending to infinity, with almost all measured in logarithmic density. This does not prove that every orbit reaches 1.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Rewards
No Prove Together bounty is promised. Erdős Problem 1135 explains that the often-repeated $500 figure was a valuation, not a specifically offered prize.
Sources and provenance
Tao, Almost all orbits of the Collatz map attain almost bounded values: exact map and limitation of the primary result (checked 2026-09-11): https://arxiv.org/abs/1909.03562
Bloom’s maintained problem catalog: current status and correction of the often-quoted $500 reward claim; its accelerated odd step is equivalent for reaching 1 (checked 2026-09-11): https://www.erdosproblems.com/1135
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/CollatzConjecture.lean
Local target: Corpus.WikipediaCollatzConjecture.collatz_conjecture
Source SHA-256: e95517fcb08fc0f37f94cc9370977584f72c57f02a58b22889c31e68b3b96bec
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For a positive integer n, define C(n) = n/2 when n is even and C(n) = 3n + 1 when n is odd. Starting from n, repeatedly apply C. Is it true that for every n ≥ 1 there is an integer m ≥ 0 for which C iterated m times sends n to 1? The starting value counts as the zeroth iterate; n
If the Collatz orbit of n reaches 1, then the orbit of 2^r*n reaches 1 for every natural r. This propagates an established convergence result; it does not assume or prove universal convergence.
If n reaches m after a Collatz steps and m reaches 1 after b steps, then n reaches 1 after a+b steps.
Every power of two 2^r reaches 1 after r Collatz steps, including r = 0.
For all natural r and n, the imported Collatz map sends 2^r*n to n after r steps. This is repeated halving, not convergence for arbitrary n.
Four elementary Collatz lemmas are now checked, using the board's imported Corpus.WikipediaCollatzConjecture.collatzStep (not a replacement definition). 1. Repeated halving: C^[r](2^r*n) = n for all natural r,n. Proof: C(2n)=n, followed by induction on r. https://provetogether.ai