Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$. The Collatz conjecture asserts that every orbit of this map eventually reaches $1$. It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$. They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$.

• 1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$, in natural density.
• 1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$, for every $\theta > 0.869$.
• 1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$.
• 2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$, in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
• 2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

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

Write $\mathrm{collatzStep}^{[k]}$ for the $k$-fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$. The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$. It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$, which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$. The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$.

For a set $A$ of positive integers and a real cutoff $x \ge 2$, the logarithmic mass of $A$ up to $x$ is

$$\mathrm{weightedLogMassReal}(x) = \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ n \in A}} \frac{1}{n}.$$

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$. Since $\sum_{n \le x} 1/n = \log x + O(1)$, all positive integers together have logarithmic density $1$, and the odd positive integers have logarithmic density $1/2$.

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$.

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

$$\lim_{x \to \infty} \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ \exists k,\ \mathrm{collatzStep}^{[k]}(n) < f(n)}} \frac{1}{n} = 1.$$

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$, which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$,

$$\frac{1}{\log x} \sum_{\substack{1 \le n \le x,\ n \text{ odd} \\ \mathrm{syracuseOrbitMin}(n) > M}} \frac{1}{n} \le \frac{C}{(\log M)^{c}}.$$

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$. The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$.

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

• Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$. This is the same definition as in the ProofAtlas source.
• Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$.
• Density. The goal uses weightedLogMassReal: a real cutoff $x$, the natural indices $0 \le n \le \lfloor x \rfloor$, weights $1/n$, and normalization by $\log x$. The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$. A short bridge between the two normalizations is part of the required work.
• Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
• Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$. For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

• Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
• ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
• Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78