ProofAtlas

First-party checked source

Source for 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. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Read the theorem overviewComplete checked Lean source · 386 Lean files · 1 evidence record · Download ZIPOpen CollatzPositiveDensity.lean

Immutable source commit: 830b9d3f38f2a8da8cd921bf6a9310dd69336fd0

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Proof and source

What is checked—and how much source supports it

Browse the counted source
Declarations covered by evidence
4
First-party Lean files
386
Lean source lines
61,169
Main recorded file
23 lines
How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence, not every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Explicit Positive-Density Collatz Convergence in Logarithmic Time

CollatzPositiveDensity.densityConstant_pos, CollatzPositiveDensity.cutoff_pos, CollatzPositiveDensity.positive_density, CollatzPositiveDensity.positive_density_ten48

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit
830b9d3f38f2a8da8cd921bf6a9310dd69336fd0
Main Lean file
CollatzPositiveDensity.lean
Main-file footprint
23 lines
File SHA-256
sha256:0670b896862f7b8a289c1e41e073ad250fd1898b5b27f6f98232e1ecb29a042a
Complete Lean closure
386 files · 61,169 lines
Toolchain
leanprover/lean4:v4.30.0-rc2
Open main Lean file Download main Lean fileDownload checker evidence (JSON)Download Apache-2.0 licenseDownload Lech Mazur notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Complete checked Lean closure

386 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

386Lean files
Search and browse all 386 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Showing all 386 files

Erdos11352 files · 16 lines
Erdos1135/ND/Fourier1 file · 39 lines
Erdos1135/ND/PositiveDensity128 files · 19,332 lines
Erdos1135/ND/Probability1 file · 17 lines
Erdos1135/Tao/Fourier29 files · 7,585 lines
Erdos1135/Tao/Probability16 files · 2,542 lines
Erdos1135/Tao/Renewal148 files · 25,269 lines
Erdos1135/Tao/Section53 files · 168 lines
Erdos1135/Tao/Section636 files · 4,791 lines
Erdos1135/Tao/Syracuse18 files · 1,330 lines
Erdos1135/Terras/Core1 file · 10 lines
Erdos1135/Terras/Density1 file · 29 lines
FormalConjectures/Wikipedia1 file · 18 lines
Package root1 file · 23 lines
Source hashMatches checked record
Lean buildPassed in recorded evidence
LicenseApache-2.0 · Lech Mazur

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Lech Mazur; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.