HEXAGONbeta

Explicit positive lower density for the Collatz Conjecture

A mix of human-written and AI-generated textHuman understanding: some partsmath.NT — Number Theory

Contributed by Kenny Lau ↗

Version 1 / Oct 14, 2026 / CC BY 4.0

Abstract

Lech Mazur proved that a positive proportion of integers nn reach 11 under the Collatz map in at most 10.46log⁡n10.46\log n steps. We give a quantitative refinement of his construction. For any X≥222287640X\ge 2^{2^{2^{2^{87640}}}}, at least X/22287640X/2^{2^{2^{87640}}} positive integers n<Xn<X reach 11 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 tt not divisible by 33. AxiomProver was used to obtain and formalize this result in Lean.

Provenance statement

This project was born out of our goal to formalize Mazur's paper, with the intent of improving the estimates. With this stated goal, AxiomProver autonomously produced the mathematics in this paper and formalized it in Lean. Although this paper was written with AI assistance, the human author is accountable for the statements and conclusions in the introduction, and summarized the main argument in Section 2 to facilitate human understanding.

Formalizations

Tools used

Axiom Math
AxiomProver

References

  1. S. Boucheron, G. Lugosi, and P. Massart, Concentration inequalities: a nonasymptotic theory of independence , Oxford University Press, Oxford, 2013.
  2. R. Durrett, Probability: theory and examples , 5th ed., Cambridge University Press, Cambridge, 2019.
  3. W. Feller, An introduction to probability theory and its applications , Vol. I, 3rd ed., Wiley, New York, 1968.
  4. W. Hoeffding, Probability inequalities for sums of bounded random variables , J. Amer. Statist. Assoc. 58 (1963), no. 301, 13--30. doi:10.1080/01621459.1963.10500830 (https://doi.org/10.1080/01621459.1963.10500830).DOI
  5. I. Krasikov and J. C. Lagarias, Bounds for the 3x+13x+1 problem using difference inequalities , Acta Arith. 109 (2003), no. 3, 237--258. doi:10.4064/aa109-3-4 (https://doi.org/10.4064/aa109-3-4).DOI
  6. M. Loève, Probability theory I , 4th ed., Graduate Texts in Mathematics, vol. 45, Springer, New York, 1977.
  7. L. Mazur, Positive lower density of Collatz predecessors , manuscript, version 1.0, September 6, 2026. https://proofatlas.ai/papers/positive-lower-density-collatz-predecessors/paper-v1.pdf.link
  8. L. Mazur, Explicit positive-density Collatz convergence in logarithmic time , manuscript, version 2.1, September 6, 2026. https://proofatlas.ai/papers/positive-density-log-time-collatz/Mazur_Explicit_Positive_Density_Collatz_Convergence_in_Logarithmic_Time_v2.pdf.link
  9. I. A. Shaik, Positive density of Collatz convergence at every rate above 3/log⁡(4/3)3/\log(4/3) , preprint, version 1.0.0, September 21, 2026. doi:10.5281/zenodo.22871622 (https://doi.org/10.5281/zenodo.22871622).DOI
  10. T. Tao, Almost all orbits of the Collatz map attain almost bounded values , Forum Math. Pi 10 (2022), e12. doi:10.1017/fmp.2022.8 (https://doi.org/10.1017/fmp.2022.8). Cited by the numbering of the corrected version arXiv:1909.03562v7 (https://arxiv.org/abs/1909.03562v7) (2026), whose Section 6 is the form used here.arXivDOI

Version history

  1. v1Submitted by Kenny LauInitial depositCurrentOct 14, 2026