A real fraction reaches 1 quickly
- What it is
- A reported Lean formalization establishes a positive lower density of starting values reaching 1 within logarithmically many ordinary Collatz steps.
- Who did it
- Lech Mazur, developed with AI agents through ProofAtlas
- What it could mean
- A simple number game has resisted mathematicians for decades. This does not solve Collatz, but it could prove that a definite share of starting numbers reach the finish line quickly.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Explicit Positive-Density Collatz Convergence in Logarithmic Time ↗See the proposed checks
Obtain the released source only in a separate ephemeral environment; verify dependency pins, public-root axioms and the exact theorem declaration; then examination the source-to-paper correspondence, explicit constants, cutoff, and the claimed ordinary-step convention.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The release claims fixed explicit constants (c>0) and (X₀) such that every (X≥ X₀) has at least (cX) positive starts (n<X) reaching 1 within ((523/50)ln n) ordinary Collatz steps. It expressly does not resolve the full Collatz conjecture. The source is consequential both as a partial result and as a current AI-assisted formalization package.
- Why this could matter
- A real fraction reaches 1 quickly The Collatz puzzle asks whether every positive integer eventually reaches 1 under a simple rule. This release claims something narrower: a fixed positive fraction reach 1 within a logarithmic number of ordinary steps, beyond a very large cutoff.
- If it holds up
- It would give number theory an explicit positive-density result with a checkable formal endpoint, while leaving the full Collatz conjecture open.
- If it does not
- The formal statement, constants, cutoff, or source-to-paper alignment would need correction; the full conjecture remains unresolved either way.
- Impact horizon
- Foundational · Number theory · Dynamical systems · Formal verification
- Version
- ProofAtlas formalization release, manuscript v2.1 dated 2026-09-06
- Why we tracked it
- a newly released, explicitly scoped Collatz partial result with a declared Lean source package, successful owning-target build transcript, and a bounded replay route; inclusion is not independent validation.
- Highest-risk dependency
- The release’s build and artifact claims are publisher assertions until independently replayed. Positive lower density with an enormous cutoff is not density-one convergence, an optimal bound, or a solution of Collatz.
- Available artifacts
- The primary release links a theorem-specific Lean source package, pinned dependencies, recorded no-sorry/axiom checks and a successful owning-target build transcript. No artifact was downloaded, executed, or replayed in this intake.
- Current boundary
- Intake record only; examination not started.