Collatz positive-density convergence, AI-developed, Lean-checked
Awaiting review
Importance: major (4 of 5)The takeaway
The first linear lower bound for Collatz-convergent integers (earlier bounds were X^0.84, then X^0.90): an explicit positive proportion of n < X reach 1 within 10.46 ln n steps. Developed mainly by AI agents, Lean-checked twice, not yet peer reviewed. The Collatz conjecture itself stays open.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 18 October 2026
Your AI and this story
- GPT-6 Astra129 days after its cutoff
- Claude Opus 5.568 days after its cutoff
- Gemini 4 Argon159 days after its cutoff
- Grok 4.798 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 68 days before it.
Key facts
- Theorem 1.1: explicit rational c > 0 and integer X₀ with #{1 ≤ n < X : τ(n) ≤ (523/50) log n} ≥ cX for every X ≥ X₀; so convergence to 1 within 10.46 log n steps holds on a set of positive lower natural density
- Prior bounds: Krasikov & Lagarias (Acta Arith. 2003) X^0.84 convergent integers ≤ X; Mazur, ‘Certified x^0.90 Lower Bounds for Collatz Predecessor Sets’ (ProofAtlas, July 17, 2026); Tao (Forum Math. Pi 2022): almost all orbits (log density) attain almost bounded values, which does not give convergence to 1
- Paper’s own limits: ‘The density bound is extremely small and the cutoff extremely large; no practical numerical range is claimed’; ‘The result does not settle the Collatz conjecture’. Axiom’s README states the thresholds as N ≥ 2^2^2^2^87640 and fraction 1/2^2^2^87640
- AI disclosure (quoted): ‘Generative AI contributed substantially to mathematical exploration, proof development, computational testing, formalization, and exposition, not only to language editing. Lech Mazur directed the AI-assisted research and is the author responsible for the manuscript and its claims. The ProofAtlas.ai harness was used for the AI-assisted research and verification workflow, with OpenAI GPT models accessed through Codex. Anthropic Claude was also used for manuscript review.’
- Mazur on X: ‘Developed primarily by AI agents using the ProofAtlas.ai harness and Codex, with some high-level guidance from me (which may or may not have helped)’
- Lean (paper §9): main theorem formalized with no admitted proof or project axiom, only propext, Classical.choice, Quot.sound; builds on earlier formalizations of Tao’s almost-boundedness and Mazur’s natural-density extension (July 21, 2026). ProofAtlas page: ‘Lean checked’, ‘Unfinished proof steps: None’, ‘Publication: Review pending’
- Axiom Math repo AxiomMath/CollatzPositiveDensity (created 2026-10-09) formalizes the theorem plus variants for other targets s coprime to 6 and t not divisible by 3, with a challenge file verified by the Lean comparator
What happened
Lech Mazur (who posted the GPT-5.6 Pro Sendov proof in August) announced on Sept 6, 2026 that a fixed positive fraction of all integers below every large enough cutoff reach 1 under the Collatz map within 10.46 ln n ordinary steps. Until then, unconditional counting results only gave sublinear numbers of convergent integers: X^0.84 (Krasikov–Lagarias 2003) and X^0.90 (Mazur’s own AI-assisted ProofAtlas paper of July 2026). Tao’s 2019 theorem is a different kind of statement: almost every orbit gets below any slowly growing function, which does not give convergence to 1. The paper combines finite ternary mixing, a weighted inverse-orbit construction from one fixed convergent seed, and a counting estimate. Both constants are given by finite expressions, but they are astronomically extreme.
The disclosure credits generative AI with the exploration, proof development, testing, formalization and exposition, through the ProofAtlas.ai harness with OpenAI GPT models in Codex, and Claude for manuscript review. ProofAtlas lists the Lean build as passed with no unfinished steps and the publication as “review pending”. On Oct 9, Axiom Math published a separate Lean formalization that also covers other targets, with a comparator-checked challenge file.
We missed this for six weeks. It was not on arXiv and had no Techmeme or press coverage. The sweep found it through Axiom’s GitHub repo (which cites the X post) while checking the AxiomMath account on Oct 18.
Why it matters
Collatz is one of the best-known open problems. This does not prove it, but it is the first result showing that convergent integers make up a positive proportion, with a logarithmic time bound. It was produced mainly by AI agents directed by a non-academic, and checked in Lean twice. No expert review or published reaction was found by Oct 18, so its standing in the field is unknown.
What is disputed or not yet verified
| Verification | Formal proof in Lean (ProofAtlas build, then an independent Axiom Math formalization with comparator check); not peer reviewed; no published expert assessment found |
|---|
Sources
4 sources from 3 sites. Numbers match the chips in the text.
4 sources: 3 primary, 1 reaction
Primary
- Paper: Explicit Positive-Density Collatz Convergence in Logarithmic Time (v2.1, PDF)proofatlas.ai, paper
- ProofAtlas formalization pageproofatlas.ai, code
- AxiomMath/CollatzPositiveDensity (independent Lean formalization)github.com, code
Reactions
- Lech Mazur on X: announcement (Sept 6, 2026)x.com, discussion
Changes
- Filed (found via AxiomMath/CollatzPositiveDensity during the evening science check; paper PDF, ProofAtlas page and X post via fxtwitter read)