/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilCollatz 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:
namespace OeisA153330Single step of the Collatz mapping.
def collatzStep (n : ℕ) : ℕ :=
if n % 2 = 0 then n / 2 else 3 * n + 1open Classical in
Number of iterations required to turn $n$ into 1 in the Collatz process,
or none if $n$ does not terminate.
noncomputable def collatzSteps (n : ℕ) : Option ℕ :=
if n = 0 then none
else if ∃ k : ℕ, (collatzStep^[k]) n = 1 then
some (sInf {k : ℕ | (collatzStep^[k]) n = 1})
else
noneopen Classical in
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.
noncomputable def a (n : ℕ) : Option ℤ :=
if n = 0 then none
else
match collatzSteps (n + 1), collatzSteps n with
| some s2, some s1 => some (s2 - s1)
| _, _ => none
Value of the sequence a at 0.
@[category test, AMS 11]
theorem a_0 : a 0 = none := ⊢ a 0 = none All goals completed! 🐙
Value of the sequence a at 1.
h1:IsLeast {k | collatzStep^[k] 1 = 1} 0h2:IsLeast {k | collatzStep^[k] 2 = 1} 1hs1:collatzSteps 1 = some 0hs2:collatzSteps 2 = some 1⊢ (match some 1, some 0 with
| some s2, some s1 => some (↑s2 - ↑s1)
| x, x_1 => none) =
some 1; All goals completed! 🐙
Value of the sequence a at 2.
h2:IsLeast {k | collatzStep^[k] 2 = 1} 1h3:IsLeast {k | collatzStep^[k] 3 = 1} 7hs2:collatzSteps 2 = some 1hs3:collatzSteps 3 = some 7⊢ (match some 7, some 1 with
| some s2, some s1 => some (↑s2 - ↑s1)
| x, x_1 => none) =
some 6; All goals completed! 🐙
Value of the sequence a at 3.
h3:IsLeast {k | collatzStep^[k] 3 = 1} 7h4:IsLeast {k | collatzStep^[k] 4 = 1} 2hs3:collatzSteps 3 = some 7hs4:collatzSteps 4 = some 2⊢ (match some 2, some 7 with
| some s2, some s1 => some (↑s2 - ↑s1)
| x, x_1 => none) =
some (-5); All goals completed! 🐙
Value of the sequence a at 4.
h4:IsLeast {k | collatzStep^[k] 4 = 1} 2h5:IsLeast {k | collatzStep^[k] 5 = 1} 5hs4:collatzSteps 4 = some 2hs5:collatzSteps 5 = some 5⊢ (match some 5, some 2 with
| some s2, some s1 => some (↑s2 - ↑s1)
| x, x_1 => none) =
some 3; All goals completed! 🐙The set of positive indices $n$ for which $a(n) = v$.
def indices (v : ℤ) : Set ℕ :=
{n : ℕ | 0 < n ∧ a n = some v}Conjecture 1: More than half of the terms are 0.
Ya-Ping Lu, May 04 2024
@[category research open, AMS 11]
theorem conjecture1 :
1 / 2 < Filter.atTop.liminf (fun n : ℕ ↦
(((Finset.Icc 1 n).filter (fun i ↦ a i = some 0)).card : ℝ) / (n : ℝ)) := ⊢ 1 / 2 < Filter.liminf (fun n ↦ ↑{i ∈ Finset.Icc 1 n | a i = some 0}.card / ↑n) Filter.atTop
All goals completed! 🐙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
@[category research open, AMS 11]
theorem conjecture2 :
indices 1 = {1} ∧
indices 6 = {2} ∧
indices 16 = {8} ∧
indices 3 = {4, 5} := ⊢ indices 1 = {1} ∧ indices 6 = {2} ∧ indices 16 = {8} ∧ indices 3 = {4, 5}
All goals completed! 🐙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).
@[category research open, AMS 11]
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 := n:ℕv:ℤhn:0 < nha:a n = some vhv:v ≠ 1 ∧ v ≠ 3 ∧ v ≠ 6⊢ ∃ x y, v.natAbs = 5 * x + 8 * y
All goals completed! 🐙Conjecture 4 (Ya-Ping Lu, 2024): 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}$.
@[category research open, AMS 11]
theorem conjecture4 (m : ℤ) (hm : m ≠ 1 ∧ m ≠ 3 ∧ m ≠ 6 ∧ m ≠ 16) :
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) := m:ℤhm:m ≠ 1 ∧ m ≠ 3 ∧ m ≠ 6 ∧ m ≠ 16⊢ Filter.Tendsto (fun n ↦ ↑{i ∈ Finset.Icc 1 n | a i = some m}.card / ↑{i ∈ Finset.Icc 1 n | a i = some (-m)}.card)
Filter.atTop (nhds 1)
All goals completed! 🐙end OeisA153330