/-
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 FormalConjecturesUtilConjectures associated with A105210
$a(1) = 393$; for $n > 1$, $a(n) = a(n-1)$ + 1 + sum of distinct prime factors of $a(n-1)$ that are $< a(n-1)$.
References:
namespace OeisA105210open Nat FinsetThe sum of distinct prime factors of $n$ that are strictly less than $n$.
def sumRelevantPrimeFactors (n : ℕ) : ℕ :=
(Nat.primeFactors n).sum (fun p => if p < n then p else 0)
The primary defining sequence a.
$a(1) = 393$; for $n > 1$, $a(n)$ = $a(n-1)$ + 1 + sum of distinct prime factors of $a(n-1)$
that are < $a(n-1)$.
def a : ℕ → ℕ
| 0 => 0
| 1 => 393
| n + 2 =>
let aPrev := a (n + 1)
aPrev + 1 + sumRelevantPrimeFactors aPrev
termination_by n => nTerm theorems verifying the first few values of the sequence against the official OEIS b-file
@[category test, AMS 11]
theorem a_1 : a 1 = 393 := ⊢ a 1 = 393 All goals completed! 🐙@[category test, AMS 11]
theorem a_2 : a 2 = 528 := ⊢ a 2 = 528 All goals completed! 🐙@[category test, AMS 11]
theorem a_3 : a 3 = 545 := ⊢ a 3 = 545 All goals completed! 🐙@[category test, AMS 11]
theorem a_4 : a 4 = 660 := ⊢ a 4 = 660 All goals completed! 🐙@[category test, AMS 11]
theorem a_5 : a 5 = 682 := ⊢ a 5 = 682 All goals completed! 🐙The transition function for these sequences: $f(n) = n + 1 + S(n)$.
def nextTermFn (n : ℕ) : ℕ :=
n + 1 + sumRelevantPrimeFactors nThe sequence starting at positive integer $k$, where seq $k$ $n$ is the $n$-th term (1-indexed). This is the general form of the sequence A105210 for a starting value $k$.
def sequenceStartingAt (k : ℕ) : ℕ → ℕ
| 0 => 0
| 1 => k
| n + 1 => nextTermFn (sequenceStartingAt k n)
termination_by n => nThe set of all terms generated by the sequence starting at $k$.
def sequenceSet (k : ℕ) : Set ℕ :=
{ m | ∃ n : ℕ, 1 ≤ n ∧ sequenceStartingAt k n = m }Cormier and Selfridge found 5 starting values for which the sequences appear to not merge. The sequences were checked up to 10^8.
@[category research open, AMS 11]
theorem conjecture_disjoint_starting_values :
∀ j k : ℕ,
j ∈ ({1, 393, 412, 668, 932} : Set ℕ) →
k ∈ ({1, 393, 412, 668, 932} : Set ℕ) →
j ≠ k →
sequenceSet j ∩ sequenceSet k = ∅ := ⊢ ∀ (j k : ℕ), j ∈ {1, 393, 412, 668, 932} → k ∈ {1, 393, 412, 668, 932} → j ≠ k → sequenceSet j ∩ sequenceSet k = ∅
All goals completed! 🐙This suggests that there may be infinitely many different (non-merging) sequences obtained by choosing different starting values.
@[category research open, AMS 11]
theorem conjecture :
∃ K : Set ℕ,
Set.Infinite K ∧
(∀ k ∈ K, 1 ≤ k) ∧
(∀ j k : ℕ,
j ∈ K → k ∈ K → j ≠ k →
sequenceSet j ∩ sequenceSet k = ∅) := ⊢ ∃ K, K.Infinite ∧ (∀ k ∈ K, 1 ≤ k) ∧ ∀ (j k : ℕ), j ∈ K → k ∈ K → j ≠ k → sequenceSet j ∩ sequenceSet k = ∅
All goals completed! 🐙end OeisA105210