Formal evidence
No public review decision is displayed for this gate.
Lean evidence record
Explicit Positive-Density Collatz Convergence in Logarithmic Time: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Lean buildpassed
Unfinished proof stepsNone
Accepted-result publicationPending
Exact recorded Lean statement
The declaration this evidence supports
theorem positive_density (X : ℕ) (hX : cutoff ≤ X) :
(densityConstant : ℝ) * X ≤ (countBelow (523 / 50) X : ℝ)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.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
positive_density- Source commit
830b9d3f38f2
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.collatz.positive_density_log_time.lean-package.v003- Declarations covered by recorded evidence
CollatzPositiveDensity.densityConstant_posCollatzPositiveDensity.cutoff_posCollatzPositiveDensity.positive_densityCollatzPositiveDensity.positive_density_ten48- Lean build
- passed
- Recorded build time
- 1523.0 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.30.0-rc2- Recorded source commit
830b9d3f38f2a8da8cd921bf6a9310dd69336fd0- Source SHA-256
sha256:0670b896862f7b8a289c1e41e073ad250fd1898b5b27f6f98232e1ecb29a042a- Statement alignment
- accepted
Lean foundations
Standard foundations used by the proof
Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.
Classical.choiceQuot.soundpropext
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Public review decisions
Accepted-result publication remains pending. This public release is not presented as a ProofAtlas accepted result; that does not establish which individual reviews are unfinished.
These are publicly visible recorded decisions for the named subjects, not a new review of this page. A decision not displayed here is not evidence that its review is unfinished. Individual decisions do not establish public accepted-result status.
Statement alignment
No public review decision is displayed for this gate.
Result boundary
No public review decision is displayed for this gate.
Public wording
No public review decision is displayed for this gate.
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.