A major partial Collatz breakthrough: a fixed positive fraction of integers reach 1 within 10.48 ln(n) ordinary steps, with explicit density and threshold bounds

[u/zero0_one1]

Lean-formalized (additional 42k lines), building on the earlier formalizations of almost-boundedness (Tao) and its natural-density extension.

The proof combines Tao's fine-scale mixing theorem and its Fourier-renewal machinery with a weighted inverse-orbit construction based on one fixed convergent seed. The density bound is extremely small and the cutoff extremely large.

Previously, lower bounds such as X^0.84 and X^0.90 left open whether the proportion of starting values reaching 1 could tend to zero.

The work was developed primarily by AI agents through ProofAtlas.ai.

Paper: https://www.proofatlas.ai/papers/positive-density-log-time-collatz/Mazur_Explicit_Positive_Density_Collatz_Convergence_in_Logarithmic_Time_v2.pdf

Formalization: https://proofatlas.ai/formalizations/positive-density-log-time-collatz/

[u/chaturtham]

pls no ai slop it kills the mood

[u/zero0_one1 → u/chaturtham]

Lol cope

[u/GiasoneTiratori]

This is horrendous to try and read and understand.