Conjectures associated with A105210

/-
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 FormalConjecturesUtil

/-!
# Conjectures 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:*
- [A105210](https://oeis.org/A105210)
-/

namespace OeisA105210

open Nat Finset

/-- The 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 => n

/-- Term 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 := by native_decide

@[category test, AMS 11]
theorem a_2 : a 2 = 528 := by native_decide

@[category test, AMS 11]
theorem a_3 : a 3 = 545 := by native_decide

@[category test, AMS 11]
theorem a_4 : a 4 = 660 := by native_decide

@[category test, AMS 11]
theorem a_5 : a 5 = 682 := by native_decide

/-- The transition function for these sequences: $f(n) = n + 1 + S(n)$. -/
def nextTermFn (n : ℕ) : ℕ :=
  n + 1 + sumRelevantPrimeFactors n

/-- The 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 => n

/-- The 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 = ∅ := by
  sorry

/--
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 = ∅) := by
  sorry

end OeisA105210

• Formalization source ↗

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.