Small Collatz lemmas become machine-checkable
- What it is
- A Lean repository formalizes finite discrepancy bounds for residue classes and harmonic arithmetic progressions in a Collatz research program.
- Who did it
- Elias De Jesús, with repository commits crediting Claude Opus 5 for portions of the revision
- What it could mean
- Formal systems can make small, exact mathematical claims inspectable while keeping the big conjecture visibly open.
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
EOC Lean Verification: harmonic discrepancy and cylinder arithmetic ↗See the proposed checks
In a separate ephemeral environment, pin commit 20fda6e, inspect the declared trust boundary and run the owning Lean targets; then compare the exact statement of harmonicapdiscrepancy with the README’s prose and verify that no conditional interface is silently used.
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 current source declares Lean formalizations of finite residue-count and harmonic arithmetic-progression discrepancy bounds, plus cylinder arithmetic. Its documentation explicitly limits these to finite or conditional infrastructure and states that the Collatz conjecture and the project’s Global Occupation Conjecture remain open.
- Why this could matter
- Small Collatz lemmas become machine-checkable Collatz research involves patterns in repeated odd-number transformations. This revision formalizes finite rules for how evenly certain residue classes appear, including a harmonic-weighted version, while explicitly not claiming to solve the famous conjecture.
- If it holds up
- It would add reusable machine-checkable building blocks and clearer boundaries between finite arithmetic facts, conditional arguments, and open questions.
- If it does not
- A declaration, dependency, or claimed scope boundary would need repair; the open Collatz problem remains open.
- Impact horizon
- Methods · Number theory · Formal verification · Dynamical systems
- Version
- main commit 20fda6ebf2c1d13b07fb64d339a55595ebeb242f, pushed 2026-09-13 11:56:27 UTC; adds harmonic packing and 8/9-drift-exclusion formalization after a same-day cylinder next-digit-counting revision.
- Why we tracked it
- The primary artifact was substantively revised today and supplies inspectable theorem declarations rather than an unsupported general Collatz claim. It is a bounded example of how a research program exposes exact claims and stated non-claims for machine checking.
- Highest-risk dependency
- A successful Lean build would establish only the declarations under its toolchain and axioms; it would not establish manuscript novelty, any bridge from finite discrepancy to real Collatz trajectories, EOC, or Collatz itself.
- Available artifacts
- Public Lean 4 repository with pinned toolchain and Mathlib manifest. The source labels its listed declarations “FORMALLY VERIFIED,” but no artifact was downloaded, built, or replayed here.
- Current boundary
- Intake record only; examination not started.