/-
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 FormalConjecturesUtilArray read by upward antidiagonals
Array read by upward antidiagonals: row $n$ ($n \ge 0$) contains the numbers $m^2 - n^2$, $m \ge n+1$.
References:
namespace OeisA105020Triangular number $T_c = c(c+1)/2$.
def triangularNumber (c : ℕ) : ℕ := Nat.choose (c + 1) 2The index $c$ of the antidiagonal containing $n$, i.e., the largest $c$ such that $T_c \le n$. This is derived from $c = \lfloor (\sqrt{8n+1} - 1) / 2 \rfloor$.
def antidiagonalIndex (n : ℕ) : ℕ :=
(Nat.sqrt (8 * n + 1) - 1) / 2
The primary defining sequence a.
Array read by upward antidiagonals: row $n$ ($n \ge 0$) contains the numbers
$m^2 - n^2$, $m \ge n+1$.
The array entry $T(i, j)$ is $(i+j+1)^2 - i^2$.
The sequence $a(n)$ is generated by reading $T(i, j)$ for $i+j=c$,
with $i$ decreasing from $c$ to $0$.
def a (n : ℕ) : ℕ :=
let c := antidiagonalIndex n
let k := n - triangularNumber c
let i := c - k
let m := c + 1
m^2 - i^2Term theorems verifying the first few values of the sequence against the official OEIS b-file
@[category test, AMS 11]
theorem a_0 : a 0 = 1 := ⊢ a 0 = 1
⊢ (have c := ((8 * 0 + 1).sqrt - 1) / 2;
have k := 0 - (c + 1).choose 2;
have i := c - k;
have m := c + 1;
m ^ 2 - i ^ 2) =
1
All goals completed! 🐙@[category test, AMS 11]
theorem a_1 : a 1 = 3 := ⊢ a 1 = 3
⊢ (have c := ((8 * 1 + 1).sqrt - 1) / 2;
have k := 1 - (c + 1).choose 2;
have i := c - k;
have m := c + 1;
m ^ 2 - i ^ 2) =
3
All goals completed! 🐙@[category test, AMS 11]
theorem a_2 : a 2 = 4 := ⊢ a 2 = 4
⊢ (have c := ((8 * 2 + 1).sqrt - 1) / 2;
have k := 2 - (c + 1).choose 2;
have i := c - k;
have m := c + 1;
m ^ 2 - i ^ 2) =
4
All goals completed! 🐙@[category test, AMS 11]
theorem a_3 : a 3 = 5 := ⊢ a 3 = 5
⊢ (have c := ((8 * 3 + 1).sqrt - 1) / 2;
have k := 3 - (c + 1).choose 2;
have i := c - k;
have m := c + 1;
m ^ 2 - i ^ 2) =
5
All goals completed! 🐙@[category test, AMS 11]
theorem a_4 : a 4 = 8 := ⊢ a 4 = 8
⊢ (have c := ((8 * 4 + 1).sqrt - 1) / 2;
have k := 4 - (c + 1).choose 2;
have i := c - k;
have m := c + 1;
m ^ 2 - i ^ 2) =
8
All goals completed! 🐙A "Goldbach Conjecture" for this sequence: when there are $n$ terms between consecutive odd integers $2n+1$ and $2n+3$ for $n > 0$, at least one will be the product of 2 primes (not necessarily distinct). Example: $n=3$ for consecutive odd integers $a(7) = 7$ and $a(11) = 9$ and of the 3 sequence entries $a(8) = 12$, $a(9) = 15$ and $a(10) = 16$ between them, one is the product of 2 primes $a(9) = 15=3*5$. - Michael Hiebl, Jul 15 2007
@[category research open, AMS 11]
theorem conjecture :
∀ (n i j : ℕ), 1 ≤ n →
a i = 2 * n + 1 →
a j = 2 * n + 3 →
j = i + n + 1 →
∃ (k : ℕ),
i < k ∧
k < j ∧
(a k).IsSemiprime := ⊢ ∀ (n i j : ℕ),
1 ≤ n →
OeisA105020.a i = 2 * n + 1 →
OeisA105020.a j = 2 * n + 3 → j = i + n + 1 → ∃ k, i < k ∧ k < j ∧ (OeisA105020.a k).IsSemiprime
All goals completed! 🐙end OeisA105020