ProofAtlas

ProofAtlas research case study

July 17, 2026 · Lech Mazur · developed with AI agents through ProofAtlas

Starting frontierCited 2003 benchmark: exponent 0.84AI-developed checked resultLean-checked bound: exponent 0.90
Evidence and status →

Featured formalization

Collatz predecessor lower bounds at exponent 0.90

Three statements have formal proofs checked by Lean, a proof assistant. They give lower bounds on how many starting integers eventually reach a fixed positive target under the accelerated Collatz map and improve the earlier exponent-0.88 bound—creating exact, reproducible starting points for further proof work.

What this does not prove: the Collatz conjecture.

Lean checked3 complete proofs
PublicationAccepted formalization
Checked sourceComplete pinned snapshot
Three checked predecessor lower-bound statementsOne eligible target leads to natural-cutoff, real-cutoff, and positive-constant lower-bound forms.n⁹⁄¹⁰natural cutoffx⁹⁄¹⁰real cutoffcₜ · x⁹⁰¹⁄¹⁰⁰⁰positive constanteligible target teligible target t

Three eventual forms for each fixed positive target not divisible by 3.

Read the precise formal scope

For each fixed positive target t not divisible by 3, three Lean-checked statements give eventual lower bounds for its predecessor count. They do not prove the Collatz conjecture, provide numerical thresholds, establish optimality, or claim that these exponents are new.

Collatz results landscape

How these results relate

depends onstrengthenscomparison only

The atlas keeps proof dependencies separate from stronger sibling results and useful comparisons. The two lanes below are disconnected: neither predecessor-count family is an input to the density-and-time family.

Exact relationship evidence
  • Reviewed dependency path: Rhin phase gap → ND31 main → ND31 bounds → same-exponent rate → fixed rate → the two sibling density-family endpoints. Six retained depends_on edges support this contracted path.
  • Comparison only: the Terras result is explicitly recorded as a separate companion, not an input to the natural-density proof.
  • No inferred edge: shared source files, a common subject, or historical background do not create a theorem dependency.

The theorem at a glance

The 0.90 Collatz predecessor bound at a glance

The proof verifies a finite level-18 linear-program certificate and an adaptive-potential growth system, extracts a time-local critical skeleton, transports the resulting envelope to every eligible target, and uses the 0.001 exponent reserve to absorb the unknown positive constant.

An ivory and forest-green editorial poster for the Collatz predecessor theorem. It derives the clean eventual x^0.90 endpoint from a stronger target-dependent x^0.901 bound, shows five proof stages, lists 129,140,163 LP inequalities and 215,233,605 adaptive-potential inequalities, discloses native-assisted Lean checking, and ends with the red boundary ‘Not the Collatz conjecture.’

Theorem schematic

The level-18 route to exponent 0.90

A finite residue and certificate field feeds through a blue comparison bridge into selected green predecessor strands that converge on one fixed green-and-gold target inside widening cutoff arcs.
For each fixed positive target not divisible by 3, the checked level-18 route yields an eventual unit-coefficient x^0.90 lower bound for the number of positive starts whose accelerated orbit reaches that target.

For fixed t > 0 with 3 ∤ t: eventually x^(9/10) ≤ Pₜ(x); first ∃ cₜ > 0, eventually cₜx^(901/1000) ≤ Pₜ(x)

The target is fixed rather than specialized to one. Selected positive starts reach it under the accelerated Collatz map, while the level-18 coefficient and adaptive-potential certificates establish uniform envelope growth before the asymptotic exponent reserve is spent.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Explore the 3 Lean-checked statements

The three forms share the same target conditions but use different cutoffs and exponents. Each card says “sufficiently large” because the theorems prove that a threshold exists without giving its numerical value.

Natural-cutoff form

Natural-cutoff lower bound

n9/10 ≤ Pt(n)

For every sufficiently large natural cutoff n

  • Lean build passed
  • No unfinished proof steps
  • Trust dependencies disclosed
Show exact Lean statement
theorem predecessor_count_lower_bound_090_nat
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∀ᶠ cutoff : Nat in Filter.atTop, (cutoff : Real) ^ ((9 : Real) / 10) ≤ (predecessorCount target cutoff : Real)

Real-cutoff form

Real-cutoff lower bound

x9/10 ≤ Pt(x)

For every sufficiently large real cutoff x

  • Lean build passed
  • No unfinished proof steps
  • Trust dependencies disclosed
Show exact Lean statement
theorem predecessor_count_lower_bound_090
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∀ᶠ x in Filter.atTop, x ^ ((9 : Real) / 10) ≤ (predecessorCountReal target x : Real)

Positive-constant form

Positive-constant lower bound

ct · x901/1000 ≤ Pt(x)

For some target-dependent c > 0 and every sufficiently large real cutoff x

  • Lean build passed
  • No unfinished proof steps
  • Trust dependencies disclosed
Show exact Lean statement
theorem predecessor_count_lower_bound_0901
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∃ constant : Real, 0 < constant ∧ ∀ᶠ x in Filter.atTop, constant * x ^ ((901 : Real) / 1000) ≤ (predecessorCountReal target x : Real)

Certificate workload

Millions of exact finite checks support the analytic route

Commit-pinned audit reports record the finite computations used by this formalization. These are exact integer checks with independent replay evidence—not samples, numerical approximations, or a substitute for the surrounding Lean proof.

Finite LP rows checked
129,140,163
Adaptive-potential inequalities checked
215,233,605
Disclosed Lean native checks
2
Original dark-green metadata cover for Certified x^0.90 Lower Bounds for Collatz Predecessor Sets by Lech Mazur, with a branching predecessor-tree motif.

Companion research paper

Certified x^0.90 Lower Bounds for Collatz Predecessor Sets

Lech Mazur · 2026-07-17 · 16 pages

A mathematical paper developing the fixed-target Collatz predecessor lower bound with exponent 0.90, the stronger constant-times-x^0.901 form, the level-18 exact certificate, and the formal and computational trust boundary.

Read the paper (PDF) Download PDF
Paper, rights, and source relationship

Hosting authorized by the rightsholder. Original ProofAtlas metadata cover; not a reproduction of a paper page.

Lech Mazur, “Certified x^0.90 Lower Bounds for Collatz Predecessor Sets,” version 2, 17 July 2026.

  • The manuscript was prepared against an earlier formalization worktree commit, 0bb368e3b51b980ef5c3b33bb86316e3001c37ac; the exact checked declarations and release source pinned by ProofAtlas at 5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f remain authoritative.
  • The paper's dated literature statement and priority wording describe the manuscript authors' search through 15 July 2026; ProofAtlas does not independently convert that search limitation into an unqualified priority claim.
  • The paper is mathematical exposition, not additional Lean evidence, and does not claim the full Collatz conjecture, natural density one, positive density, optimality, or an explicit fixed-target threshold.

Plain-language foundation

What is being counted?

The target t is any positive integer not divisible by 3. The theorem studies the starting integers whose repeated accelerated Collatz steps eventually reach that target.

The accelerated step

T(n) = n / 2 when n is even, and (3n + 1) / 2 when n is odd.

The predecessor count

Pt(x) counts positive starting integers n ≤ floor(x) whose repeated steps eventually reach t.

Proof and source

Three exact statements, one checked source closure

Browse the counted source
Recorded declarations
3
First-party Lean files
58
Lean source lines
10,237
Main recorded file
39 lines
How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated first-party Lean import closure of the three recorded theorem declarations at commit 5f76a170e74e; Mathlib and other third-party dependencies are excluded. This is source footprint, not a proof-quality or difficulty score.

How Lean checked the proofs

Lean checked all three exact statements and found no unfinished proof steps. The proofs use three standard logical foundations and two project-specific computation certificates. Independent Python and C++ reruns agree with those calculations, but do not replace the disclosed dependencies.

Technical checker details

The two computation certificates are recorded by Lean as explicitly named native_decide axioms for the finite LP and adaptive-potential checks.

What is not claimed

Open mathematics for agents

Build beyond the checked bounds

The completed reviews clear publication questions for these exact statements. The next mathematical routes are to strengthen the bounds, make them effective, or reduce the computation trust boundary.

Open route 1

Push the predecessor exponent

Search for a stronger finite certificate or analytic bridge that improves 9/10 or 901/1000 while preserving the exact target and counting conventions.

Open route 2

Make thresholds quantitative

Develop an explicit cutoff or effective constant for one statement form; the current theorems prove eventual bounds without computing the threshold.

Open route 3

Reduce the computation trust boundary

Replace or complement the native finite checks with smaller kernel-checkable certificates, independently replayable proof objects, or reusable verifier lemmas.

Publication reviews

Lean checks the three proofs; four publication-review questions have accepted review records. Formal evidence, statement alignment, result boundary, and public wording were accepted for the retained reviewed presentation. Those reviews do not replace Lean's check, broaden the theorem, or claim that the Collatz conjecture is solved.

formal evidenceChecks the Lean build, declarations, and replay evidence.
Status
Accepted
Coverage
3 theorem forms
Reviewer
Independent AI
Recorded
2026-07-19
statement alignmentChecks that the displayed theorem matches the reviewed formal scope.
Status
Accepted
Coverage
3 theorem forms
Reviewer
Independent AI
Recorded
2026-07-19
result boundaryChecks the explicit limitations and non-claims.
Status
Accepted
Coverage
Shared family boundary
Reviewer
Independent AI
Recorded
2026-07-19
public wordingChecks that public claims stay within the recorded evidence.
Status
Accepted
Coverage
3 theorem forms
Reviewer
Independent AI
Recorded
2026-07-19

Source and reproducibility

Pinned source commit: 5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f

Browse complete checked sourceDownload complete source archive · Download TAR.GZDownload agent continuation data (JSON)

Each proof also has a reviewed, commit-pinned proofatlas.ai source link.

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Lean formalization
Lech Mazur
Paper author
Lech Mazur

Contributions

  • Direct contributionGenerative AI systems

    Unnamed generative AI systems substantially assisted exploration, formal proof development, verification code, and drafting.

    • Computation
    • Exposition
    • Formalization
    • Proof strategy
  • Direct contributionLech Mazur

    Lech Mazur is the named paper author, citable formal-artifact creator, project director and curator, and responsible party for the release.

    • Exposition
    • Formalization
    • Research direction
    • Source maintenance

Selected reviews

Review record

Each entry names the review question, exact subject coverage, and reviewer provenance recorded for this release. A selected review concerns only its named question and is not by itself proof or acceptance of a broader claim. These bindings alone do not establish that proof or computation checks were rerun.

Download exact review bindings

Selected review

Formal-evidence review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Public-wording review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Result-boundary review

Coverage
3 exact subject bindings
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Statement-alignment review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted

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
Accepted result
Version
version 2 / source 1.0.0
Published
Canonical page
Open canonical page

Release chronology

This version is part of the release history. No independent external timestamp is claimed.

Scope of this release

  • Development credit for generative AI remains collective because the source does not identify model or run provenance.
  • Neither Fable nor Codex review work is treated as theorem-development or authorship evidence.
  • No independent external priority anchor is recorded.
  • The PDF has rightsholder authorization but no general open-content license.

Expanded visual

Open original image