Kenny Lau

math.NT — Number Theory

Explicit positive lower density for the Collatz Conjecture

Contributed by Kenny Lau

Lech Mazur proved that a positive proportion of integers $n$ reach $1$ under the Collatz map in at most $10.46\log n$ steps. We give a quantitative refinement of his construction. For any $X\ge 2^{2^{2^{2^{87640}}}}$, at least $X/2^{2^{2^{87640}}}$ positive integers $n<X$ reach $1$ within $\floor{10.46\log n}$ ordinary steps, and $\floor{3.4881\log n}$ accelerated steps. We also obtain results for paths that include any prescribed integer $t$ not divisible by $3$. AxiomProver was used to obtain and formalize this result in Lean.