As of: 2026-10-18 22:10 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/p/2026-09-06-lechmazur-collatz-positive-density/

# Lech Mazur: AI agents prove a positive fraction of integers reach 1 under Collatz in 10.46 ln n steps (Lean-formalized)

Lech Mazur (@LechMazur), X, 2026-09-06.
Source: https://x.com/LechMazur/status/2096464472973975782

## 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).
>
> 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/


## Cited in

- 2026-09-06: [Collatz positive-density convergence, AI-developed, Lean-checked](https://postcutoff.com/e/2026-09-06-collatz-positive-density-log-time-mazur-codex/)