153330.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 4 contain sorry, 0 declared as axioms

Collatz step differences

Differences in adjacent elements of the sequence quantifying the steps needed for $n$ to converge to 1 in the Collatz Conjecture. $$a(n) = \mathrm{A006577}(n+1) - \mathrm{A006577}(n)$$ for $n > 0$.

References:

A153330

Imports (1)

FormalConjecturesUtil

def OeisA153330.collatzStep Single step of the Collatz mapping line 36 source
Source documentation
Single step of the Collatz mapping.

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, HMod.hMod, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, HMul.hMul
10 instances, coercions and auxiliary constants left out.
```
def collatzStep (n : ℕ) : ℕ :=
…
```
def OeisA153330.collatzSteps Number of iterations required to turn $n$ into 1 in the Collatz process, or none if $n$ does not terminate line 42 source
Source documentation
Number of iterations required to turn $n$ into 1 in the Collatz process, or none if $n$ does not terminate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Option
Proof uses: ite, Eq, OfNat.ofNat, Option.none, Exists, Nat.iterate, OeisA153330.collatzStep, Classical.propDecidable, Option.some, InfSet.sInf, Set.ofPred
3 instances, coercions and auxiliary constants left out.
```
noncomputable def collatzSteps (n : ℕ) : Option ℕ :=
…
```
def OeisA153330.a The sequence $a(n) = \mathrm{A006577}(n+1) - \mathrm{A006577}(n)$ for $n > 0$, or none if either $n$ or $n+1$ does not terminate line 52 source
Source documentation
The sequence $a(n) = \mathrm{A006577}(n+1) - \mathrm{A006577}(n)$ for $n > 0$, or none if either $n$ or $n+1$ does not terminate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Option, Int
Proof uses: ite, Eq, OfNat.ofNat, Option.none, OeisA153330.a.match_1, OeisA153330.collatzSteps, HAdd.hAdd, Option.some, HSub.hSub
8 instances, coercions and auxiliary constants left out.
```
noncomputable def a (n : ℕ) : Option ℤ :=
…
```
theorem OeisA153330.a_0 Value of the sequence a at 0 line 61 source
Source documentation
Value of the sequence a at 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, OeisA153330.a, OfNat.ofNat, Nat, Option.none
Proof uses: Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem a_0 : a 0 = none := by rfl
…
```
Mentions: OeisA153330.a
theorem OeisA153330.a_1 Value of the sequence a at 1 line 65 source
Source documentation
Value of the sequence a at 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, OeisA153330.a, OfNat.ofNat, Nat, Option.some
Proof uses: IsLeast, Set.ofPred, Nat.iterate, OeisA153330.collatzStep, And.intro, Membership.mem, Set, lowerBounds, rfl, of_eq_true, LE.le, Eq.trans, True, forall_congr, implies_congr, Eq.refl, implies_true, Decidable.byContradiction, Not, LT.lt and 33 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem a_1 : a 1 = some 1 := by
…
```
Mentions: OeisA153330.a
theorem OeisA153330.a_2 Value of the sequence a at 2 line 81 source
Source documentation
Value of the sequence a at 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, OeisA153330.a, OfNat.ofNat, Nat, Option.some
Proof uses: IsLeast, Set.ofPred, Nat.iterate, OeisA153330.collatzStep, And.intro, Membership.mem, Set, lowerBounds, Eq.refl, Decidable.byContradiction, LE.le, Not, LT.lt, False, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.symm and 27 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
theorem a_2 : a 2 = some 6 := by
…
```
Mentions: OeisA153330.a
theorem OeisA153330.a_3 Value of the sequence a at 3 line 100 source
Source documentation
Value of the sequence a at 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, OeisA153330.a, OfNat.ofNat, Nat, Option.some, Neg.neg
Proof uses: IsLeast, Set.ofPred, Nat.iterate, OeisA153330.collatzStep, And.intro, Membership.mem, Set, lowerBounds, Eq.refl, Decidable.byContradiction, LE.le, Not, dite, False, LT.lt, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true and 27 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
theorem a_3 : a 3 = some (-5) := by
…
```
Mentions: OeisA153330.a
theorem OeisA153330.a_4 Value of the sequence a at 4 line 119 source
Source documentation
Value of the sequence a at 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, OeisA153330.a, OfNat.ofNat, Nat, Option.some
Proof uses: IsLeast, Set.ofPred, Nat.iterate, OeisA153330.collatzStep, And.intro, Membership.mem, Set, lowerBounds, Eq.refl, Decidable.byContradiction, LE.le, Not, dite, False, LT.lt, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true and 27 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
theorem a_4 : a 4 = some 3 := by
…
```
Mentions: OeisA153330.a
def OeisA153330.indices The set of positive indices $n$ for which $a(n) = v$ line 137 source
Source documentation
The set of positive indices $n$ for which $a(n) = v$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Set, Nat
Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Eq, Option, OeisA153330.a, Option.some
2 instances, coercions and auxiliary constants left out.
```
def indices (v : ℤ) : Set ℕ :=
…
```
theorem OeisA153330.conjecture1 Conjecture 1: More than half of the terms are 0 sorry line 145 source
Source documentation
Conjecture 1: More than half of the terms are 0.
- Ya-Ping Lu, May 04 2024
depends on sorry what this means
Statement uses: LT.lt, Real, HDiv.hDiv, OfNat.ofNat, Nat, Filter.liminf, Finset.card, Finset.filter, Eq, Option, Int, OeisA153330.a, Option.some, Finset.Icc, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture1 :
    1 / 2 < Filter.atTop.liminf (fun n : ℕ ↦
      (((Finset.Icc 1 n).filter (fun i ↦ a i = some 0)).card : ℝ) / (n : ℝ)) := by
…
```
Mentions: OeisA153330.a
theorem OeisA153330.conjecture2 Conjecture 2: 1, 6 and 16 appear only once and 3 appears twice in the sequence, i.e., $a(1) = 1$, $a(2) = 6$, $a(4) = a(5) = 3$, and $a(8) = 16$ sorry line 156 source
Source documentation
Conjecture 2: 1, 6 and 16 appear only once and 3 appears twice in the sequence, i.e., $a(1) = 1$, $a(2) = 6$, $a(4) = a(5) = 3$, and $a(8) = 16$.
- Ya-Ping Lu, May 04 2024
depends on sorry what this means
Statement uses: And, Eq, Set, Nat, OeisA153330.indices, OfNat.ofNat, Int, Singleton.singleton, Insert.insert
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture2 :
    indices 1 = {1} ∧
    indices 6 = {2} ∧
    indices 16 = {8} ∧
    indices 3 = {4, 5} := by
…
```
Mentions: OeisA153330.indices
theorem OeisA153330.conjecture3 Conjecture 3 (Ya-Ping Lu, 2024): Except 1, 3 and 6, the absolute value of all terms can be written as $5x + 8y$ for $x, y \in \mathbb{N}$ sorry line 170 source
Source documentation
Conjecture 3 (Ya-Ping Lu, 2024): Except 1, 3 and 6, the absolute value of all terms can be written as $5x + 8y$ for $x, y \in \mathbb{N}$. (Note: in the OEIS comment, "x and y are integers" means $x$ and $y$ have the same sign, i.e., $|v| = 5x + 8y$ with $x, y \ge 0$, since every integer is a $\mathbb{Z}$-linear combination of 5 and 8).

depends on sorry what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, Eq, Option, OeisA153330.a, Option.some, And, Ne, Exists, Int.natAbs, HAdd.hAdd, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture3 (n : ℕ) (v : ℤ) (hn : 0 < n) (ha : a n = some v)
    (hv : v ≠ 1 ∧ v ≠ 3 ∧ v ≠ 6) :
    ∃ x y : ℕ, v.natAbs = 5 * x + 8 * y := by
…
```
Mentions: OeisA153330.a
theorem OeisA153330.conjecture4 Documented declaration: conjecture4 sorry line 181 source
Source documentation
Conjecture 4 (Ya-Ping Lu, 2024): For an $m$ that appears in the sequence, the ratio of the number of terms with value $m$ to that of $-m$ approaches 1 as $n \to \infty$, for any $|m| \notin \{1, 3, 6, 16\}$.

depends on sorry what this means
Statement uses: Int, Not, Membership.mem, Nat, Finset, Insert.insert, OfNat.ofNat, Singleton.singleton, Int.natAbs, Exists, And, LT.lt, Eq, Option, OeisA153330.a, Option.some, Filter.Tendsto, Real, HDiv.hDiv, Finset.card and 5 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture4 (m : ℤ) (hm : m.natAbs ∉ ({1, 3, 6, 16} : Finset ℕ))
    (hocc : ∃ n, 0 < n ∧ a n = some m) :
    Filter.atTop.Tendsto
      (fun n : ℕ ↦
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some m)).card : ℝ) /
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some (-m))).card : ℝ))
      (nhds 1) := by
…
```
Mentions: OeisA153330.a