FormalConjectures.OEIS.«100474»

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

$a(1) = 1$; $a(n)$ is the smallest integer such that $a(n) + a(n-1)$ has the first $n$ distinct prime factors not used before in this construction.

References:

A100474

namespace OeisA100474

The $n$-th triangular number.

def triangular (n : ℕ) : ℕ := n * (n + 1) / 2

The primary defining sequence a.

noncomputable def a : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 =>
    (Finset.Ico (triangular (n + 1) - 1) (triangular (n + 2) - 1)).prod (Nat.nth Nat.Prime) -
      a (n + 1)



@[category API, AMS 11]
lemma nth_prime_five : Nat.nth Nat.Prime 5 = 13 := by⊢ Nat.nth Nat.Prime 5 = 13
  have h1 : (13).Prime := by decideh1:Nat.Prime 13⊢ Nat.nth Nat.Prime 5 = 13h1:Nat.Prime 13⊢ Nat.nth Nat.Prime 5 = 13
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_six : Nat.nth Nat.Prime 6 = 17 := by⊢ Nat.nth Nat.Prime 6 = 17
  have h1 : (17).Prime := by decideh1:Nat.Prime 17⊢ Nat.nth Nat.Prime 6 = 17h1:Nat.Prime 17⊢ Nat.nth Nat.Prime 6 = 17
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_seven : Nat.nth Nat.Prime 7 = 19 := by⊢ Nat.nth Nat.Prime 7 = 19
  have h1 : (19).Prime := by decideh1:Nat.Prime 19⊢ Nat.nth Nat.Prime 7 = 19h1:Nat.Prime 19⊢ Nat.nth Nat.Prime 7 = 19
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_eight : Nat.nth Nat.Prime 8 = 23 := by⊢ Nat.nth Nat.Prime 8 = 23
  have h1 : (23).Prime := by decideh1:Nat.Prime 23⊢ Nat.nth Nat.Prime 8 = 23h1:Nat.Prime 23⊢ Nat.nth Nat.Prime 8 = 23
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_nine : Nat.nth Nat.Prime 9 = 29 := by⊢ Nat.nth Nat.Prime 9 = 29
  have h1 : (29).Prime := by decideh1:Nat.Prime 29⊢ Nat.nth Nat.Prime 9 = 29h1:Nat.Prime 29⊢ Nat.nth Nat.Prime 9 = 29
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_ten : Nat.nth Nat.Prime 10 = 31 := by⊢ Nat.nth Nat.Prime 10 = 31
  have h1 : (31).Prime := by decideh1:Nat.Prime 31⊢ Nat.nth Nat.Prime 10 = 31h1:Nat.Prime 31⊢ Nat.nth Nat.Prime 10 = 31
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_eleven : Nat.nth Nat.Prime 11 = 37 := by⊢ Nat.nth Nat.Prime 11 = 37
  have h1 : (37).Prime := by decideh1:Nat.Prime 37⊢ Nat.nth Nat.Prime 11 = 37h1:Nat.Prime 37⊢ Nat.nth Nat.Prime 11 = 37
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_twelve : Nat.nth Nat.Prime 12 = 41 := by⊢ Nat.nth Nat.Prime 12 = 41
  have h1 : (41).Prime := by decideh1:Nat.Prime 41⊢ Nat.nth Nat.Prime 12 = 41h1:Nat.Prime 41⊢ Nat.nth Nat.Prime 12 = 41
  exact Nat.nth_count h1All goals completed! 🐙



@[category API, AMS 11]
lemma nth_prime_thirteen : Nat.nth Nat.Prime 13 = 43 := by⊢ Nat.nth Nat.Prime 13 = 43
  have h1 : (43).Prime := by decideh1:Nat.Prime 43⊢ Nat.nth Nat.Prime 13 = 43h1:Nat.Prime 43⊢ Nat.nth Nat.Prime 13 = 43
  exact Nat.nth_count h1All goals completed! 🐙

Value of the sequence a at 1.

@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1 rflAll goals completed! 🐙

Value of the sequence a at 2.


@[category test, AMS 11]
theorem a_2 : a 2 = 5 := by⊢ a 2 = 5
  change (Finset.Ico 0 2).prod (Nat.nth Nat.Prime) - a 1 = 5⊢ (Finset.Ico 0 2).prod (Nat.nth Nat.Prime) - a 1 = 5
  rw [Finset.prod_Ico_succ_top (by⊢ 0 ≤ 1⊢ (∏ k ∈ Finset.Ico 0 1, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 1 - a 1 = 5 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 0 1, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 1 - a 1 = 5)]⊢ (∏ k ∈ Finset.Ico 0 1, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 1 - a 1 = 5
  rw [Finset.prod_Ico_succ_top (by⊢ 0 ≤ 0⊢ (∏ k ∈ Finset.Ico 0 0, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 0 * Nat.nth Nat.Prime 1 - a 1 = 5 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 0 0, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 0 * Nat.nth Nat.Prime 1 - a 1 = 5)]⊢ (∏ k ∈ Finset.Ico 0 0, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 0 * Nat.nth Nat.Prime 1 - a 1 = 5
  simp only [Finset.Ico_self, Finset.prod_empty, one_mul]⊢ Nat.nth Nat.Prime 0 * Nat.nth Nat.Prime 1 - a 1 = 5
  rw [Nat.nth_prime_zero_eq_two,⊢ 2 * Nat.nth Nat.Prime 1 - a 1 = 5⊢ 2 * 3 - a 1 = 5 Nat.nth_prime_one_eq_three⊢ 2 * 3 - a 1 = 5⊢ 2 * 3 - a 1 = 5]⊢ 2 * 3 - a 1 = 5
  rflAll goals completed! 🐙

Value of the sequence a at 3.


@[category test, AMS 11]
theorem a_3 : a 3 = 380 := by⊢ a 3 = 380
  change (Finset.Ico 2 5).prod (Nat.nth Nat.Prime) - a 2 = 380⊢ (Finset.Ico 2 5).prod (Nat.nth Nat.Prime) - a 2 = 380
  rw [a_2⊢ (Finset.Ico 2 5).prod (Nat.nth Nat.Prime) - 5 = 380⊢ (Finset.Ico 2 5).prod (Nat.nth Nat.Prime) - 5 = 380]⊢ (Finset.Ico 2 5).prod (Nat.nth Nat.Prime) - 5 = 380
  rw [Finset.prod_Ico_succ_top (by⊢ 2 ≤ 4⊢ (∏ k ∈ Finset.Ico 2 4, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 4 - 5 = 380 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 2 4, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 4 - 5 = 380)]⊢ (∏ k ∈ Finset.Ico 2 4, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 4 - 5 = 380
  rw [Finset.prod_Ico_succ_top (by⊢ 2 ≤ 3⊢ (∏ k ∈ Finset.Ico 2 3, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 2 3, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380)]⊢ (∏ k ∈ Finset.Ico 2 3, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380
  rw [Finset.prod_Ico_succ_top (by⊢ 2 ≤ 2⊢ (∏ k ∈ Finset.Ico 2 2, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 2 * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 2 2, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 2 * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380)]⊢ (∏ k ∈ Finset.Ico 2 2, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 2 * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380
  simp only [Finset.Ico_self, Finset.prod_empty, one_mul]⊢ Nat.nth Nat.Prime 2 * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380
  rw [Nat.nth_prime_two_eq_five,⊢ 5 * Nat.nth Nat.Prime 3 * Nat.nth Nat.Prime 4 - 5 = 380⊢ 5 * 7 * 11 - 5 = 380 Nat.nth_prime_three_eq_seven,⊢ 5 * 7 * Nat.nth Nat.Prime 4 - 5 = 380⊢ 5 * 7 * 11 - 5 = 380 Nat.nth_prime_four_eq_eleven⊢ 5 * 7 * 11 - 5 = 380⊢ 5 * 7 * 11 - 5 = 380]⊢ 5 * 7 * 11 - 5 = 380
  rflAll goals completed! 🐙

Value of the sequence a at 4.


@[category test, AMS 11]
theorem a_4 : a 4 = 96197 := by⊢ a 4 = 96197
  change (Finset.Ico 5 9).prod (Nat.nth Nat.Prime) - a 3 = 96197⊢ (Finset.Ico 5 9).prod (Nat.nth Nat.Prime) - a 3 = 96197
  rw [a_3⊢ (Finset.Ico 5 9).prod (Nat.nth Nat.Prime) - 380 = 96197⊢ (Finset.Ico 5 9).prod (Nat.nth Nat.Prime) - 380 = 96197]⊢ (Finset.Ico 5 9).prod (Nat.nth Nat.Prime) - 380 = 96197
  rw [Finset.prod_Ico_succ_top (by⊢ 5 ≤ 8⊢ (∏ k ∈ Finset.Ico 5 8, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 8 - 380 = 96197 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 5 8, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 8 - 380 = 96197)]⊢ (∏ k ∈ Finset.Ico 5 8, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 8 - 380 = 96197
  rw [Finset.prod_Ico_succ_top (by⊢ 5 ≤ 7⊢ (∏ k ∈ Finset.Ico 5 7, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 5 7, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197)]⊢ (∏ k ∈ Finset.Ico 5 7, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197
  rw [Finset.prod_Ico_succ_top (by⊢ 5 ≤ 6⊢ (∏ k ∈ Finset.Ico 5 6, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 =
  96197 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 5 6, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 =
  96197)]⊢ (∏ k ∈ Finset.Ico 5 6, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 =
  96197
  rw [Finset.prod_Ico_succ_top (by⊢ 5 ≤ 5⊢ (∏ k ∈ Finset.Ico 5 5, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 5 * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 *
      Nat.nth Nat.Prime 8 -
    380 =
  96197 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 5 5, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 5 * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 *
      Nat.nth Nat.Prime 8 -
    380 =
  96197)]⊢ (∏ k ∈ Finset.Ico 5 5, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 5 * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 *
      Nat.nth Nat.Prime 8 -
    380 =
  96197
  simp only [Finset.Ico_self, Finset.prod_empty, one_mul]⊢ Nat.nth Nat.Prime 5 * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197
  rw [nth_prime_five,⊢ 13 * Nat.nth Nat.Prime 6 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197⊢ 13 * 17 * 19 * 23 - 380 = 96197 nth_prime_six,⊢ 13 * 17 * Nat.nth Nat.Prime 7 * Nat.nth Nat.Prime 8 - 380 = 96197⊢ 13 * 17 * 19 * 23 - 380 = 96197 nth_prime_seven,⊢ 13 * 17 * 19 * Nat.nth Nat.Prime 8 - 380 = 96197⊢ 13 * 17 * 19 * 23 - 380 = 96197 nth_prime_eight⊢ 13 * 17 * 19 * 23 - 380 = 96197⊢ 13 * 17 * 19 * 23 - 380 = 96197]⊢ 13 * 17 * 19 * 23 - 380 = 96197
  rflAll goals completed! 🐙

Value of the sequence a at 5.


@[category test, AMS 11]
theorem a_5 : a 5 = 58546472 := by⊢ a 5 = 58546472
  change (Finset.Ico 9 14).prod (Nat.nth Nat.Prime) - a 4 = 58546472⊢ (Finset.Ico 9 14).prod (Nat.nth Nat.Prime) - a 4 = 58546472
  rw [a_4⊢ (Finset.Ico 9 14).prod (Nat.nth Nat.Prime) - 96197 = 58546472⊢ (Finset.Ico 9 14).prod (Nat.nth Nat.Prime) - 96197 = 58546472]⊢ (Finset.Ico 9 14).prod (Nat.nth Nat.Prime) - 96197 = 58546472
  rw [Finset.prod_Ico_succ_top (by⊢ 9 ≤ 13⊢ (∏ k ∈ Finset.Ico 9 13, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 13 - 96197 = 58546472 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 9 13, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 13 - 96197 = 58546472)]⊢ (∏ k ∈ Finset.Ico 9 13, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 13 - 96197 = 58546472
  rw [Finset.prod_Ico_succ_top (by⊢ 9 ≤ 12⊢ (∏ k ∈ Finset.Ico 9 12, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 9 12, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472)]⊢ (∏ k ∈ Finset.Ico 9 12, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472
  rw [Finset.prod_Ico_succ_top (by⊢ 9 ≤ 11⊢ (∏ k ∈ Finset.Ico 9 11, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 -
    96197 =
  58546472 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 9 11, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 -
    96197 =
  58546472)]⊢ (∏ k ∈ Finset.Ico 9 11, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 -
    96197 =
  58546472
  rw [Finset.prod_Ico_succ_top (by⊢ 9 ≤ 10⊢ (∏ k ∈ Finset.Ico 9 10, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 9 10, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472)]⊢ (∏ k ∈ Finset.Ico 9 10, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472
  rw [Finset.prod_Ico_succ_top (by⊢ 9 ≤ 9⊢ (∏ k ∈ Finset.Ico 9 9, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 9 * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 *
        Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472 decideAll goals completed! 🐙⊢ (∏ k ∈ Finset.Ico 9 9, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 9 * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 *
        Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472)]⊢ (∏ k ∈ Finset.Ico 9 9, Nat.nth Nat.Prime k) * Nat.nth Nat.Prime 9 * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 *
        Nat.nth Nat.Prime 12 *
      Nat.nth Nat.Prime 13 -
    96197 =
  58546472
  simp only [Finset.Ico_self, Finset.prod_empty, one_mul]⊢ Nat.nth Nat.Prime 9 * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 -
    96197 =
  58546472
  rw [nth_prime_nine,⊢ 29 * Nat.nth Nat.Prime 10 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472 nth_prime_ten,⊢ 29 * 31 * Nat.nth Nat.Prime 11 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472 nth_prime_eleven,⊢ 29 * 31 * 37 * Nat.nth Nat.Prime 12 * Nat.nth Nat.Prime 13 - 96197 = 58546472⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472 nth_prime_twelve,⊢ 29 * 31 * 37 * 41 * Nat.nth Nat.Prime 13 - 96197 = 58546472⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472 nth_prime_thirteen⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472]⊢ 29 * 31 * 37 * 41 * 43 - 96197 = 58546472
  rflAll goals completed! 🐙

After $a(2) = 5$, is there another prime?

@[category research open, AMS 11]
theorem conjecture : answer(sorry) ↔ ∃ n > 2, (a n).Prime := by⊢ True ↔ ∃ n > 2, Nat.Prime (a n)
  sorryAll goals completed! 🐙

What is the next semiprime in the sequence after $a(11)$?

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-a100474-next-semiprime/blob/d7781751918e63fd1268b15525bf9554c92fdd4d/lean/OeisA100474NextSemiprimeFC.lean#L1285-L1288"]
theorem next_semiprime :
    answer(3852669607062814427999374038085094563026983841699038416757537720951140990693348082633155462564082456461927363575765861495986901576629) =
      a (sInf {n : ℕ | 11 < n ∧ (a n).IsSemiprime}) := by⊢ 3852669607062814427999374038085094563026983841699038416757537720951140990693348082633155462564082456461927363575765861495986901576629 =
  a (sInf {n | 11 < n ∧ (a n).IsSemiprime})
  sorryAll goals completed! 🐙

end OeisA100474