Formal evidence
An independent reviewer must inspect the recorded build, declarations, unfinished-proof-step check, and disclosed foundations.
ProofAtlas research case study
Starting frontierEarlier bounds: descent or sublinear counts→Formalization candidateA positive fraction reaches 1 within 10.46 ln(n) steps
Evidence and status →Number theory · dynamical systems · formal theorem
Explicit Positive-Density Collatz Convergence in Logarithmic Time
A fixed explicit positive fraction of the integers below every sufficiently large cutoff reaches 1 within 10.46 ln n ordinary Collatz steps. The full Collatz conjecture remains open.
Scope: There are fixed explicitly defined c > 0 and X₀ such that every natural X ≥ X₀ has at least cX positive integers n < X reaching 1 within (523/50) ln n ordinary Collatz steps. The same c and X₀ also satisfy the weaker 10.48 clock.
Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Exact formal proposition
Hypotheses and conclusion
theorem positive_density (X : ℕ) (hX : cutoff ≤ X) :
(densityConstant : ℝ) * X ≤ (countBelow (523 / 50) X : ℝ)Result boundary
What this theorem does—and does not—establish
There are fixed explicitly defined c > 0 and X₀ such that every natural X ≥ X₀ has at least cX positive integers n < X reaching 1 within (523/50) ln n ordinary Collatz steps. The same c and X₀ also satisfy the weaker 10.48 clock.
- The full Collatz conjecture remains open: positive lower natural density does not imply convergence for every positive start or density-one convergence to 1.
- The endpoint counts strictly below X and bounds the number of ordinary, unaccelerated steps inclusively; it does not assert an exact asymptotic density or counting formula.
- The explicitly defined coefficient and cutoff are not practical numerical bounds.
- The checked declaration does not establish every claim in the companion paper or a historical-priority claim.
Companion note: Positive Lower Density of Collatz Predecessors extends the discussion to fixed positive targets not divisible by 3 and gives a conditional density-one convergence criterion. It is a separate paper; this paper and its logarithmic-time result are unchanged.
Companion research paper
Explicit Positive-Density Collatz Convergence in Logarithmic Time
The paper gives a fixed explicit positive rational c and a fixed explicit natural-number cutoff X₀. For every natural X ≥ X₀, at least cX positive integers n < X reach 1 within 10.46 ln n ordinary Collatz steps. This establishes positive lower natural density with explicit constants; it does not resolve the full Collatz conjecture.
Author-authorized early release. This fixed paper package first appeared while independent presentation review was pending; hosting it does not mark the Lean result accepted.
Read the paper (PDF) Download PDFDownload the complete licensed theorem-specific Lean source release, dependency pins, and recorded checks (ZIP)
Paper, rights, and source relationship
Hosting authorized by the rightsholder. Original ProofAtlas metadata cover; not a reproduced paper page or proof evidence.
Lech Mazur, “Explicit Positive-Density Collatz Convergence in Logarithmic Time,” manuscript v2.1, September 6, 2026.
- The exact Lean endpoint counts positive n strictly below a natural X, uses natural logarithms, and counts each ordinary step separately: n/2 for even n and 3n+1 for odd n. The 10.48 bound is a weaker corollary of 10.46.
- The linked artifact retains the successful owning-target lake --rehash build transcript, clean source provenance, no-sorry results and axiom checks of all four public roots for theorem-specific source 830b9d3f38f2a8da8cd921bf6a9310dd69336fd0. Pinned Mathlib caches were reused; no all-dependency cold rebuild, independent LeanChecker replay, smallest-possible-proof claim, or paper-wide review is asserted.
- Manuscript v2.1 preserves the mathematical body, bibliography, authorship and AI disclosure of v2.0; its version/date and source-package links are updated. The formal source is reduced to the public-root dependency closure. Mathematical acceptance and paper presentation review are separately recorded and do not follow from packaging or a credit snapshot.
- The density constant is extremely small and the cutoff extremely large. No practical numerical range, density-one convergence to 1, optimality, historical priority, or solution of the full Collatz conjecture is claimed.
Paper overview
Explicit positive-density Collatz convergence in logarithmic time
Author-supplied explanation, not proof evidence. In the image, M denotes the paper’s root bound 𝓜 and H denotes B = E(J) + ⌊2β(J)/3⌋; m is unchanged. The linked Lean evidence covers the exact public declarations.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Formal theorem publication status
Publication review
Accepted-result publication remains pending
Lean has checked the exact source; this public release is not presented as a ProofAtlas accepted result. The linked evidence page shows individual review decisions where they are publicly available. The requirements below describe publication coverage, not a count of unfinished reviews. Independent AI, human, or mixed reviewers may examine the build evidence, statement alignment, result boundary, and public wording. Review does not replace Lean's check or broaden the theorem.
Statement alignment
The formal declaration must be reviewed against the theorem wording and its exact variant.
Result boundary
The limits must be checked so the page cannot imply a broader theorem.
Public wording
The explanation, infographic labels, and source presentation need independent review.
Canonical source
The permanent source link and downloadable files must be approved for public citation.
Accepted result
After the four reviews and source route are ready, an accepted-result record must bind them to this exact formalization.
Credit for this release
Contributors and roles
Authorship and other contributions are recorded separately for this version.
Contributions
- Direct contributionOpenAI Codex
OpenAI GPT models accessed through Codex contributed to mathematical exploration, proof development, computational testing, formalization, and exposition in the ProofAtlas.ai harness. No model version is inferred.
- Computation
- Exposition
- Formalization
- Proof strategy
- Supporting contributionAnthropic Claude
Anthropic Claude was used for manuscript review. This source-reported manuscript review is not a current ProofAtlas independent review gate, accepted-result review, or formal proof replay.
- Exposition
- Direct contributionLech Mazur
Lech Mazur is the named paper author, directed the AI-assisted research, and is responsible for the manuscript and its claims.
- Exposition
- Research direction
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
Versions and public record
- Release
- Paper release
- Version
- manuscript v2.1 of September 6, 2026
- Published
- Canonical page
- Open canonical page
- Earlier release
credit.release.positive-density-log-time-collatz.v002
Release chronology
This version is part of the release history. No independent external timestamp is claimed.
Scope of this release
- Independent paper-to-formal-statement alignment and current publication review remain separate. Claude’s source-reported manuscript review grants no ProofAtlas review status.
- Positive lower natural density of convergence within 10.46 ln n ordinary steps does not establish density-one convergence, practical cutoffs, optimality, priority, or the full Collatz conjecture.
- The exact AI model versions are not specified in the manuscript disclosure and are not inferred.
- The linked artifact retains the successful owning-target lake --rehash build transcript, clean source provenance, no-sorry results and axiom checks of all four public roots for theorem-specific source 830b9d3f38f2a8da8cd921bf6a9310dd69336fd0. Pinned Mathlib caches were reused; no all-dependency cold rebuild, independent LeanChecker replay, smallest-possible-proof claim, or paper-wide review is asserted.
- The paper and infographic have hosting permission, with no general open-content license. The source archive retains its separate Apache-2.0 license and third-party notices.
- The v2.1 mathematical manuscript body, bibliography, authorship and source-stated AI roles are unchanged; this packaging and hosting successor does not create a new scholarly contribution or event. Historical source pins are provenance, not claimed ancestry of the parentless slim repository.