1. FormalConjectures
  2. OEIS
  3. «372761»
/- 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

Unique realization of odd primes $p \notin {3, 5}$ by continued fraction values

$a(n)$ is the denominator of the finite continued fraction $$\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}}$$

References:

    A372761

    arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

namespace OeisA372761open scoped Natopen Rat

Recursive helper computing the continued fraction denominator $R_k(n)$ for $2 \le k \le n-1$, where $R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$ with base case $R_{n-1}(n) = (n-1) - \frac{n}{n+4}$.

def continuedFractionDenominator (n k : ℕ) : ℚ := if n ≤ 2 then 0 else if 2 ≤ k ∧ k ≤ n - 1 then if k = n - 1 then (k : ℚ) - (n : ℚ) / (n + 4 : ℚ) else let R_next := continuedFractionDenominator n (k + 1) if R_next = 0 then 0 else (k : ℚ) - (k + 1 : ℚ) / R_next else 0 termination_by n - k

Denominator of the continued fraction $$ \frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}} $$

def a (n : ℕ) : ℕ := if n < 3 then 0 -- Sequence starts at n=3. else (1 / continuedFractionDenominator n 2).den⊢ (if 3 < 3 then 0 else (1 / if 3 ≤ 2 then 0 else if 2 ≤ 2 ∧ 2 ≤ 3 - 1 then if 2 = 3 - 1 then ↑2 - ↑3 / (↑3 + 4) else have R_next := continuedFractionDenominator 3 (2 + 1); if R_next = 0 then 0 else ↑2 - (↑2 + 1) / R_next else 0).den) = 11; All goals completed! 🐙⊢ (if ¬(if 4 ≤ 2 then 0 else if 2 ≤ 3 ∧ 3 ≤ 4 - 1 then if 3 = 4 - 1 then ↑3 - ↑4 / (↑4 + 4) else have R_next := continuedFractionDenominator 4 (3 + 1); if R_next = 0 then 0 else ↑3 - (↑3 + 1) / R_next else 0) = 0 → (2 - 3 / if 4 ≤ 2 then 0 else if 2 ≤ 3 ∧ 3 ≤ 4 - 1 then if 3 = 4 - 1 then ↑3 - ↑4 / (↑4 + 4) else have R_next := continuedFractionDenominator 4 (3 + 1); if R_next = 0 then 0 else ↑3 - (↑3 + 1) / R_next else 0) = 0 then 1 else (if (if 4 ≤ 2 then 0 else if 2 ≤ 3 ∧ 3 ≤ 4 - 1 then if 3 = 4 - 1 then ↑3 - ↑4 / (↑4 + 4) else have R_next := continuedFractionDenominator 4 (3 + 1); if R_next = 0 then 0 else ↑3 - (↑3 + 1) / R_next else 0) = 0 then 0 else 2 - 3 / if 4 ≤ 2 then 0 else if 2 ≤ 3 ∧ 3 ≤ 4 - 1 then if 3 = 4 - 1 then ↑3 - ↑4 / (↑4 + 4) else have R_next := continuedFractionDenominator 4 (3 + 1); if R_next = 0 then 0 else ↑3 - (↑3 + 1) / R_next else 0).num.natAbs) = 4; All goals completed! 🐙⊢ (if ¬(if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 → ¬(3 - 4 / if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 → (2 - 3 / if (if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 then 1 else (if ¬(if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 → (3 - 4 / if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 then 0 else 2 - 3 / if (if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if 5 ≤ 2 then 0 else if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then if 4 = 5 - 1 then ↑4 - ↑5 / (↑5 + 4) else have R_next := continuedFractionDenominator 5 (4 + 1); if R_next = 0 then 0 else ↑4 - (↑4 + 1) / R_next else 0).num.natAbs) = 7; All goals completed! 🐙⊢ (if ¬(if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → ¬(4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → ¬(3 - 4 / if (if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → (2 - 3 / if ¬(if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → (4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if (if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 1 else (if ¬(if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → ¬(4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → (3 - 4 / if (if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 2 - 3 / if ¬(if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 → (4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if (if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if 6 ≤ 2 then 0 else if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then if 5 = 6 - 1 then ↑5 - ↑6 / (↑6 + 4) else have R_next := continuedFractionDenominator 6 (5 + 1); if R_next = 0 then 0 else ↑5 - (↑5 + 1) / R_next else 0).num.natAbs) = 13; All goals completed! 🐙⊢ (if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(3 - 4 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (2 - 3 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 1 else (if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (3 - 4 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 2 - 3 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → ¬(5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 3 - 4 / if ¬(if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 → (5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 4 - 5 / if (if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0) = 0 then 0 else 5 - 6 / if 7 ≤ 2 then 0 else if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then if 6 = 7 - 1 then ↑6 - ↑7 / (↑7 + 4) else have R_next := continuedFractionDenominator 7 (6 + 1); if R_next = 0 then 0 else ↑6 - (↑6 + 1) / R_next else 0).num.natAbs) = 31; All goals completed! 🐙

Conjecture: Except for 3 and 5, all odd primes appear in the sequence once. - Thomas Scheuerle, May 11 2024

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/372761.wip.lean#L733"] theorem exists_unique_a_eq_prime : ∀ p : ℕ, Nat.Prime p ∧ p % 2 = 1 ∧ p ≠ 3 ∧ p ≠ 5 → ∃! n, n ≥ 3 ∧ a n = p := ⊢ ∀ (p : ℕ), Nat.Prime p ∧ p % 2 = 1 ∧ p ≠ 3 ∧ p ≠ 5 → ∃! n, n ≥ 3 ∧ OeisA372761.a n = p All goals completed! 🐙end OeisA372761