/-
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 FormalConjecturesUtilRealization of primes $p \equiv \pm 1 \pmod{10}$ by continued fraction denominators
$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}{-4}}}}}}$$
References:
arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
namespace OeisA363347open Rat NatHelper function for a, which computes the denominator $R_k(n)$ of the continued fraction expression. For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: $$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ The base case is $R_{n-1}(n) = (n-1) - \frac{n}{-4}$.
def continuedFractionDenominator (n k : ℕ) : ℚ :=
if n ≤ 2 then 0
else
-- The recursive descent involves terms from $k=n-1$ down to $k=2$.
if 2 ≤ k ∧ k ≤ n - 1 then
-- Base Case: k = n - 1.
if k = n - 1 then
-- R_{n-1} = (n-1) + n/4
(k : ℚ) + (n : ℚ) / 4
-- Recursive Step: 2 <= k < n - 1.
else
let R_next := continuedFractionDenominator n (k + 1)
-- R_k = k - (k+1) / R_{k+1}
(k : ℚ) - (k + 1 : ℚ) / R_next
else 0
termination_by n - kDenominator of the continued fraction $$\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{-4}}}}}} $$ The value of the continued fraction is $C_n = 1/R_2(n)$. If $R_2(n) = N/D$ in reduced form, $C_n = D/N$. The sequence $a(n)$ is the denominator of the final fraction, which is $\vert N \vert$.
def a (n : ℕ) : ℕ :=
if n ≤ 2 then 0 -- The sequence is indexed starting from $n=3$.
else
let R2 := continuedFractionDenominator n 2
R2.num.natAbs⊢ (if 3 ≤ 2 then 0
else
have R2 :=
if 3 ≤ 2 then 0
else
if 2 ≤ 2 ∧ 2 ≤ 3 - 1 then
if 2 = 3 - 1 then ↑2 + ↑3 / 4
else
have R_next := continuedFractionDenominator 3 (2 + 1);
↑2 - (↑2 + 1) / R_next
else 0;
R2.num.natAbs) =
11; All goals completed! 🐙⊢ (2 -
3 /
if 4 ≤ 2 then 0
else
if 2 ≤ 3 ∧ 3 ≤ 4 - 1 then
if 3 = 4 - 1 then ↑3 + ↑4 / 4
else
have R_next := continuedFractionDenominator 4 (3 + 1);
↑3 - (↑3 + 1) / R_next
else 0).num.natAbs =
5; All goals completed! 🐙⊢ (2 -
3 /
(3 -
4 /
if 5 ≤ 2 then 0
else
if 2 ≤ 4 ∧ 4 ≤ 5 - 1 then
if 4 = 5 - 1 then ↑4 + ↑5 / 4
else
have R_next := continuedFractionDenominator 5 (4 + 1);
↑4 - (↑4 + 1) / R_next
else 0)).num.natAbs =
31; All goals completed! 🐙⊢ (2 -
3 /
(3 -
4 /
(4 -
5 /
if 6 ≤ 2 then 0
else
if 2 ≤ 5 ∧ 5 ≤ 6 - 1 then
if 5 = 6 - 1 then ↑5 + ↑6 / 4
else
have R_next := continuedFractionDenominator 6 (5 + 1);
↑5 - (↑5 + 1) / R_next
else 0))).num.natAbs =
11; All goals completed! 🐙⊢ (2 -
3 /
(3 -
4 /
(4 -
5 /
(5 -
6 /
if 7 ≤ 2 then 0
else
if 2 ≤ 6 ∧ 6 ≤ 7 - 1 then
if 6 = 7 - 1 then ↑6 + ↑7 / 4
else
have R_next := continuedFractionDenominator 7 (6 + 1);
↑6 - (↑6 + 1) / R_next
else 0)))).num.natAbs =
59; All goals completed! 🐙Conjecture: The sequence contains all prime numbers which end with a 1 or 9 (i.e., primes $p \equiv 1$ or $9 \pmod{10}$).
A formal proof has been found with the methods described in arxiv/2605.22763.
@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/363347.wip.lean#L825"]
theorem exists_a_eq_prime :
∀ p : ℕ, (p.Prime ∧ (p ≡ 1 [MOD 10] ∨ p ≡ 9 [MOD 10])) → ∃ n : ℕ, a n = p := ⊢ ∀ (p : ℕ), Nat.Prime p ∧ (p ≡ 1 [MOD 10] ∨ p ≡ 9 [MOD 10]) → ∃ n, OeisA363347.a n = p
All goals completed! 🐙end OeisA363347