Array read by upward antidiagonals

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

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

namespace OeisA105020

/--
Triangular number $T_c = c(c+1)/2$.
-/
def triangularNumber (c : ℕ) : ℕ := Nat.choose (c + 1) 2

/--
The 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^2

/-- Term 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 := by
  unfold a antidiagonalIndex triangularNumber
  norm_num

@[category test, AMS 11]
theorem a_1 : a 1 = 3 := by
  unfold a antidiagonalIndex triangularNumber
  norm_num

@[category test, AMS 11]
theorem a_2 : a 2 = 4 := by
  unfold a antidiagonalIndex triangularNumber
  norm_num

@[category test, AMS 11]
theorem a_3 : a 3 = 5 := by
  unfold a antidiagonalIndex triangularNumber
  norm_num

@[category test, AMS 11]
theorem a_4 : a 4 = 8 := by
  unfold a antidiagonalIndex triangularNumber
  norm_num

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

end OeisA105020

• 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.