Lech Mazur: AI agents prove a positive fraction of integers reach 1 under Collatz in 10.46 ln n steps (Lean-formalized)
Lech Mazur @LechMazurX
Why it matters
Announcement (~204k views) of the first linear lower bound for Collatz-convergent integers, developed mainly by AI agents via ProofAtlas and Codex.
Summary
Posted 05:04 UTC on Sept 6, 2026; ~204k views and ~500 likes by Oct 18. States the theorem, contrasts it with earlier X^0.84 and X^0.90 bounds, says it is Lean-formalized (42k additional lines) and was “developed primarily by AI agents using the ProofAtlas.ai harness and Codex”. Links the paper and formalization.
Archived text
ANNOUNCEMENT: An AI milestone on one of maths’ most famous unsolved problems: COLLATZ.
For every sufficiently large X, at least cX positive integers n < X reach 1 within 10.46 ln(n) ordinary Collatz steps, for one fixed c > 0.
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.
Lean-formalized (42k additional lines), building on earlier formalizations of almost-boundedness (Tao) and its natural-density extension.
Developed primarily by AI agents using the http://ProofAtlas.ai harness and Codex, with some high-level guidance from me (which may or may not have helped).
Formalization: https://proofatlas.ai/formalizations/positive-density-log-time-collatz/