Determinants of 2 X 2 matrices… to Denominators of $\sum_{k=1}^n…

TheoremDeterminants of 2 X 2 matrices of non-overlapping blocks of 4 consecutive primes #

$a(n) = p_{4n-3}p_{4n} - p_{4n-2}p_{4n-1}$ where $p_k$ is the k-th prime number (1-indexed).

References: - A117027

Quoted from FormalConjectures/OEIS/117027.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 4 test statements and 7 API statements, counted here but not shown.

`OeisA117027.conjecture`

Open: stated without proof.

This suggests the ratio is approaching a limit close to 0.87.

Formalized as: The sequence of ratios $P(N)/Neg(N)$ converges to a limit L, and L is in the interval (0.8, 0.9).

theorem conjecture :
  ∃ L : ℝ, Tendsto ratioSeq atTop (nhds L) ∧ 0.8 < L ∧ L < 0.9

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/117027.lean, line 130.

Sources

LeanOeisA117027.conjecture

TheoremNumber of primes in $n$-th row of triangle $k^2 - k + p_n$#

$a(n)$ is the number of primes in the $n$-th row of the triangle $T(n, k) = k^2 - k + p_n$ for $1 \le k \le n$, where $p_n$ is the $n$-th prime ($p_1=2, p_2=3, \dots$).

References: - A117531

Quoted from FormalConjectures/OEIS/117531.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.

`OeisA117531.conjecture`

Open: stated without proof.

Conjecture: $a(n) < n$ for $n > 13$.

theorem conjecture (n : ℕ) (h : n > 13) : a n < n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/117531.lean, line 127.

Sources

LeanOeisA117531.conjecture

TheoremLeast $k$ such that cyclotomic polynomial $\Phi_k(n)$ is prime #

$a(n) = \min \{k \in \mathbb{N} \mid 0 < k \wedge \text{Prime}(|\Phi_k(n)|) \}$, where $\Phi_k(n)$ is the $k$-th cyclotomic polynomial evaluated at $n$.

References: - A117545

Quoted from FormalConjectures/OEIS/117545.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.

`OeisA117545.conjecture`

Open: stated without proof.

Is $a(n)$ defined for all $n \ge 1$? That is, for every $n \ge 1$, does there exist $k > 0$ such that $|\Phi_k(n)|$ is prime?

theorem conjecture (n : ℕ) (hn : 0 < n) :
    ∃ k > 0, ((Polynomial.cyclotomic k ℤ).eval (n : ℤ)).natAbs.Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/117545.lean, line 117.

Sources

LeanOeisA117545.conjecture

TheoremSum of Fermat number and Mersenne number minus 1: $2^{2^n} + 2^n - 1$#

Define $F(n) = 2^{2^n} + 1$ (the $n$-th Fermat number) and $M(n) = 2^n - 1$ (the $n$-th Mersenne number). Then $a(n) = F(n) + M(n) - 1 = 2^{2^n} + 2^n - 1$.

References: - A119563

Quoted from FormalConjectures/OEIS/119563.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.

`OeisA119563.conjecture`

Open: stated without proof.

The first 5 entries are primes. Are there infinitely many primes in this sequence?

theorem conjecture : Set.Infinite {n : ℕ | (a n).Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/119563.lean, line 59.

Sources

LeanOeisA119563.conjecture

TheoremLeast $k \ge 1$ such that $2 \cdot n^k - 1$ is prime #

$a(n) = \min \{k \ge 1 \mid \text{Prime}(2 \cdot n^k - 1)\}$ for $n \ge 2$.

References: - A119591

Quoted from FormalConjectures/OEIS/119591.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 7 test statements, counted here but not shown.

`OeisA119591.conjecture`

Open: stated without proof.

Is $a(n)$ defined for all $n \ge 2$? That is, does there exist $k > 0$ such that $2 \cdot n^k - 1$ is prime?

theorem conjecture (n : ℕ) (hn : 2 ≤ n) : ∃ k > 0, (2 * n ^ k - 1).Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/119591.lean, line 131.

Sources

LeanOeisA119591.conjecture

TheoremHalf-Fibonacci sequence #

$a(0) = 1, a(1) = 3$; for $n \ge 2$, $a(n) = f(a(n-1)) + f(a(n-2))$ where $f(x) = x/2$ if $x$ is even and $f(x) = x$ if $x$ is odd.

References: - A120424

Quoted from FormalConjectures/OEIS/120424.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 open. It also has 5 test statements, counted here but not shown.

`OeisA120424.conjecture1`

Open: stated without proof.

Conjecture (1): The natural density of even terms in the sequence is $1/2$.

theorem conjecture1 :
    Filter.Tendsto (fun n : ℕ => ((Finset.filter (fun k => a k % 2 = 0) (Finset.range n)).card
        : ℝ) / (n : ℝ))
      Filter.atTop (nhds (1 / 2 : ℝ))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/120424.lean, line 66.

`OeisA120424.conjecture2`

Open: stated without proof.

Conjecture (2): There are infinitely many consecutive pairs that differ by 1.

theorem conjecture2 :
    Set.Infinite {n : ℕ | a (n + 1) = a n + 1 ∨ a n = a (n + 1) + 1}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/120424.lean, line 75.

Sources

LeanOeisA120424.conjecture1 · OeisA120424.conjecture2

TheoremRatio of product of GCDs to product of factorials of floor divisions #

\[a(n) = \frac{\prod_{j=1}^n \prod_{k=1}^n \gcd(j,k)}{\prod_{k=1}^n (\lfloor n/k \rfloor!)^k}\]

References: - A129365

Quoted from FormalConjectures/OEIS/129365.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 4 solved. It also has 5 test statements, counted here but not shown.

`OeisA129365.conjecture1`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a129365-conjectures/blob/9c0201540c337733d6b8afb2aff209f5489c122a/lean/OeisA129365FC.lean#L234-L395.

Conjecture (1): $a(n)$ is always an integer (the denominator divides the numerator).

Proof summary:

Let $c(n) = \prod_{j=1}^n \prod_{k=1}^n (j,k)$ be the numerator. Observe that

\[\textrm{ord}(c(n), p) = \left\lfloor \frac{n}{p} \right\rfloor^2 + \left\lfloor \frac{n}{p^2} \right\rfloor^2 + ...\]

proven similar to Legendre's formula for $\textrm{ord}(n!, p)$.

Next let $d(n) = \prod_{k=1}^n (\lfloor n/k \rfloor!)^k$ be the denominator. Observe that

\[\textrm{ord}(d(n), p) = \sum_{k=1}^n k\,\textrm{ord}(\lfloor n/k \rfloor, p) = \sum_{k=1}^n \sum_{r \geq 1} k \left\lfloor \frac{\lfloor n/p^r \rfloor}{k} \right\rfloor.\]

Combining the two gives:

\[\textrm{ord}(a(n), p) = \sum_{r \geq 1} \sum_{k=1}^n \left(\left\lfloor \frac{n}{p^r} \right\rfloor \textrm{mod } k\right).\]

Defining $b(m) = \sum_{k=1}^m m \textrm{ mod } k$, we obtain $\textrm{ord}(a(n), p) = \sum_{r \geq 1} b(\lfloor n/p^r \rfloor)$.

As $b(m) \geq 0$, $\textrm{ord}(a(n), p)$ is non-negative for any $p$, so $a(n)$ is an integer.

theorem conjecture1 (n : ℕ) (hn : 0 < n) :
    ((Finset.Icc 1 n).prod fun k => (n / k).factorial ^ k) ∣
      ((Finset.Icc 1 n).prod fun j => (Finset.Icc 1 n).prod fun k => Nat.gcd j k)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/129365.lean, line 88.

`OeisA129365.conjecture2`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a129365-conjectures/blob/9c0201540c337733d6b8afb2aff209f5489c122a/lean/OeisA129365FC.lean#L234-L395.

Conjecture (2): If $p$ is a prime, then $p \mid a(n)$ if and only if $p \le n/3$.

Proof summary:

We use the formula shown above: $\textrm{ord}(a(n), p) = \sum_{r \geq 1} b(\lfloor n/p^r \rfloor)$ where $b(m) = \sum_{k=1}^m m \textrm{ mod } k$.

If $p ∣ a(n)$ then $b(\lfloor n/p^r \rfloor) ≥ 1$ for some $r ≥ 1$. Since b(m) = 0$ for $m \leq 2$, we must have $n / p^r \geq 3$. If the inequality holds for $r \geq 1$, it must be true for $r = 1$. Hence $n \geq 3p$, proving the conjecture.

theorem conjecture2 (n p : ℕ) (hn : 0 < n) (hp : p.Prime) :
    (∃ m : ℕ, a n = m ∧ p ∣ m) ↔ p ≤ n / 3

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/129365.lean, line 110.

`OeisA129365.conjecture3`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a129365-conjectures/blob/9c0201540c337733d6b8afb2aff209f5489c122a/lean/OeisA129365FC.lean#L234-L395.

Conjecture (3): For each positive integer $n$, prime $p$, and $0 \le k < p$, $\mathrm{ord}_p(a(np)) = \mathrm{ord}_p(a(np + k))$.

Proof summary:

This follows from the formula shown above: $\textrm{ord}(a(n), p) = \sum_{r \geq 1} b(\lfloor n/p^r \rfloor)$ where $b(m) = \sum_{k=1}^m m \textrm{ mod } k$.

Since $k < p$, we have $\lfloor (np + k)/p^r \rfloor = \lfloor np/p^r \rfloor$ for every $r \geq 1$, proving the claim.

theorem conjecture3 (n p k : ℕ) (hn : 0 < n) (hp : p.Prime) (hk : k < p) :
    padicValRat p (a (n * p)) = padicValRat p (a (n * p + k))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/129365.lean, line 131.

`OeisA129365.conjecture4`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a129365-conjectures/blob/9c0201540c337733d6b8afb2aff209f5489c122a/lean/OeisA129365FC.lean#L234-L395.

Conjecture (4): Let $b(n) = \mathrm{A004125}(n) = \sum_{k=1}^n (n \bmod k)$. Then $\mathrm{ord}_p(a(np)) = \sum_{i \ge 0} b(\lfloor n/p^i \rfloor)$.

Proof summary:

This follows directly from the formula shown at the beginning: $\textrm{ord}(a(n), p) = \sum_{r \geq 1} b(\lfloor n/p^r \rfloor)$ where $b(m) = \sum_{k=1}^m m \textrm{ mod } k$.

theorem conjecture4 (n p : ℕ) (hn : 0 < n) (hp : p.Prime) :
    padicValRat p (a (n * p)) = ∑' i : ℕ, (b (n / p ^ i) : ℤ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/129365.lean, line 149.

Sources

LeanOeisA129365.conjecture1 · OeisA129365.conjecture2 · OeisA129365.conjecture3 · OeisA129365.conjecture4

TheoremOdious primes minus evil primes among first $n$ primes #

$a(n)$ is the number of primes with odd binary weight (odious primes) among the first $n$ primes minus the number with even binary weight (evil primes).

References: - A130911

Quoted from FormalConjectures/OEIS/130911.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.

`OeisA130911.conjecture`

Open: stated without proof.

Shevelev conjectures that $a(n) \ge 0$ for $n > 3$.

theorem conjecture (n : ℕ) (hn : 3 < n) : a n ≥ 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/130911.lean, line 98.

Sources

LeanOeisA130911.conjecture

TheoremRecurrence involving LCM: $a(n) = x(n+1)/x(n) - 2$#

$a(n) = x(n+1)/x(n) - 2$ where $x(1)=1$ and $x(n) = 2 x(n-1) + \operatorname{lcm}(x(n-1),n)$ for $n > 1$.

References: - A135508

Quoted from FormalConjectures/OEIS/135508.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.

`OeisA135508.conjecture`

Open: stated without proof.

Conjecture: For prime $p$ such that $p-2$ is not a prime, $a(p-1) = p$. - Bill McEachen, Sep 26 2025

theorem conjecture (p : ℕ) (hp : p.Prime) (hp_twin : ¬ (p - 2).Prime) : a (p - 1) = p

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/135508.lean, line 68.

Sources

LeanOeisA135508.conjecture

TheoremNumber of Abelian cubes of length $3n$ over an alphabet of size 3 #

An Abelian cube is a string of the form $x x' x''$ with $|x| = |x'| = |x''|$ and $x$ is a permutation of $x'$ and $x''$. The number of Abelian cubes of length $3n$ over an alphabet of size 3 is given by

\[a(n) = \sum_{k=0}^n \binom{n}{k}^3 \sum_{j=0}^k \binom{k}{j}^3.\]

References: - A141057

Quoted from FormalConjectures/OEIS/141057.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 solved. It also has 7 test statements, counted here but not shown.

`OeisA141057.conjecture1`

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-full-50usd-ant-j0j0g4uzligm1k41/oeis_a141057_supercongruence_conjecture/Submission/Spec.lean#L955.

Conjecture: the supercongruences $a(n \cdot p^k) \equiv a(n \cdot p^{k-1}) \pmod{p^{3k}}$ hold for primes $p \ge 5$ and positive integers $n$ and $k$.

theorem conjecture1 (p k n : ℕ) (hp : p.Prime) (h_p_ge_5 : 5 ≤ p) (h_k_pos : 1 ≤ k)
    (h_n_pos : 1 ≤ n) :
    (a (n * p ^ k) : ℤ) ≡ a (n * p ^ (k - 1)) [ZMOD (p ^ (3 * k))]

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/141057.lean, line 65.

`OeisA141057.conjecture2`

Solved: stated here; a Lean proof is at https://github.com/JENW1N/complete-math-solutions/blob/8b9db1d8c0ded5398d5e4e4bbdf8f2ec14ce5c23/proofs/BalaA141057Conjecture.lean#L1416.

Conjecture (Peter Bala, 2022): The supercongruences $a(n \cdot p^k) \equiv a(n \cdot p^{k-1}) \pmod{p^{3k}}$ hold for the integer-indexed extension $a(n)$ for all $n \in \mathbb{Z} \setminus \{0\}$, primes $p \ge 5$, and $k \ge 1$.

Proved in Lean by Jensen Kohlmeyer and Liam Kruer, extending the positive-index proof by Epoch Research.

theorem conjecture2 (p k : ℕ) (n : ℤ) (hp : p.Prime) (h_p_ge_5 : 5 ≤ p) (h_k_pos : 1 ≤ k)
    (hn : n ≠ 0) :
    aInt (n * (p ^ k : ℤ)) ≡ aInt (n * (p ^ (k - 1) : ℤ)) [ZMOD (p ^ (3 * k) : ℤ)]

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/141057.lean, line 102.

Sources

LeanOeisA141057.conjecture1 · OeisA141057.conjecture2

TheoremFactorial distance to nearest square #

The sequence is defined as

\[a(n) = \mathrm{round}\left(\frac{\mathrm{round}(\sqrt{n!})}{\left|(\mathrm{round}(\sqrt{n!}))^2 - n!\right|}\right)\]

for $n \ge 2$.

References: - A145355

Quoted from FormalConjectures/OEIS/145355.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.

`OeisA145355.conjecture`

Open: stated without proof.

This sequence suggests that the distance between a factorial and the closest power is tightly bounded.

theorem conjecture : ∃ C : ℕ, ∀ n : ℕ, 2 ≤ n → a n ≤ C

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/145355.lean, line 81.

Sources

LeanOeisA145355.conjecture

TheoremCollatz step differences #

Differences in adjacent elements of the sequence quantifying the steps needed for $n$ to converge to 1 in the Collatz Conjecture.

\[a(n) = \mathrm{A006577}(n+1) - \mathrm{A006577}(n)\]

for $n > 0$.

References: - A153330

Quoted from FormalConjectures/OEIS/153330.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 4 open. It also has 5 test statements, counted here but not shown.

`OeisA153330.conjecture1`

Open: stated without proof.

Conjecture 1: More than half of the terms are 0. - Ya-Ping Lu, May 04 2024

theorem conjecture1 :
    1 / 2 < Filter.atTop.liminf (fun n : ℕ ↦
      (((Finset.Icc 1 n).filter (fun i ↦ a i = some 0)).card : ℝ) / (n : ℝ))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/153330.lean, line 145.

`OeisA153330.conjecture2`

Open: stated without proof.

Conjecture 2: 1, 6 and 16 appear only once and 3 appears twice in the sequence, i.e., $a(1) = 1$, $a(2) = 6$, $a(4) = a(5) = 3$, and $a(8) = 16$. - Ya-Ping Lu, May 04 2024

theorem conjecture2 :
    indices 1 = {1} ∧
    indices 6 = {2} ∧
    indices 16 = {8} ∧
    indices 3 = {4, 5}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/153330.lean, line 156.

`OeisA153330.conjecture3`

Open: stated without proof.

Conjecture 3 (Ya-Ping Lu, 2024): Except 1, 3 and 6, the absolute value of all terms can be written as $5x + 8y$ for $x, y \in \mathbb{N}$. (Note: in the OEIS comment, "x and y are integers" means $x$ and $y$ have the same sign, i.e., $|v| = 5x + 8y$ with $x, y \ge 0$, since every integer is a $\mathbb{Z}$-linear combination of 5 and 8).

theorem conjecture3 (n : ℕ) (v : ℤ) (hn : 0 < n) (ha : a n = some v)
    (hv : v ≠ 1 ∧ v ≠ 3 ∧ v ≠ 6) :
    ∃ x y : ℕ, v.natAbs = 5 * x + 8 * y

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/153330.lean, line 170.

`OeisA153330.conjecture4`

Open: stated without proof.

Conjecture 4 (Ya-Ping Lu, 2024): For an $m$ that appears in the sequence, the ratio of the number of terms with value $m$ to that of $-m$ approaches 1 as $n \to \infty$, for any $|m| \notin \{1, 3, 6, 16\}$.

theorem conjecture4 (m : ℤ) (hm : m.natAbs ∉ ({1, 3, 6, 16} : Finset ℕ))
    (hocc : ∃ n, 0 < n ∧ a n = some m) :
    Filter.atTop.Tendsto
      (fun n : ℕ ↦
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some m)).card : ℝ) /
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some (-m))).card : ℝ))
      (nhds 1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/153330.lean, line 181.

Sources

LeanOeisA153330.conjecture1 · OeisA153330.conjecture2 · OeisA153330.conjecture3 · OeisA153330.conjecture4

TheoremRepresentations as $p + 2^x + 7 \cdot 2^y$ with $p \equiv 5 \pmod 6$#

Number of ways to write the $n$-th positive odd integer in the form $p + 2^x + 7 \cdot 2^y$ with $p$ a prime congruent to $5 \bmod 6$ and $x, y$ positive integers.

\[a(n) = \left|\left\{(p, x, y) : p + 2^x + 7 \cdot 2^y = 2n - 1 \text{ with } p \text{ prime}, p \equiv 5 \pmod 6, x, y \in \mathbb{Z}^+\right\}\right|.\]

References: - A157225 - Z.-W. Sun, "Mixed sums of primes and other terms", arXiv preprint arXiv:0901.3075 [math.NT], 2009.

Quoted from FormalConjectures/OEIS/157225.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved. It also has 6 test statements, counted here but not shown.

`OeisA157225.conjecture`

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/main/runs/oeis-full-50usd-ant-j0j0g4uzligm1k41/oeis_157225_conjecture_0/Submission/Spec.lean.

On Feb. 24, 2009, Zhi-Wei Sun conjectured that $a(n) = 0$ if and only if $n < 11$ or $n \in \{13, 16, 992\}$; in other words, except for $25, 31, 1983$, any odd integer greater than $20$ can be written as the sum of a prime congruent to $5 \bmod 6$, a positive power of $2$ and seven times a positive power of $2$.

Answer: false, for n = 716993899 we have a(n) = 0. See T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arxiv/2608.11941.

theorem conjecture :
    ¬ ∀ n : ℕ, 0 < n → (a n = 0 ↔ n < 11 ∨ n = 13 ∨ n = 16 ∨ n = 992)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/157225.lean, line 86.

Sources

LeanOeisA157225.conjecture

TheoremRepresentations as $p + 2^x + 11 \cdot 2^y$ with $p \equiv 1 \pmod 6$#

Number of ways to write the $n$-th positive odd integer in the form $p + 2^x + 11 \cdot 2^y$ with $p$ a prime congruent to $1 \bmod 6$ and $x, y$ positive integers.

\[a(n) = \left|\left\{(p, x, y) : p + 2^x + 11 \cdot 2^y = 2n - 1 \text{ with } p \text{ prime}, p \equiv 1 \pmod 6, x, y \in \mathbb{Z}^+\right\}\right|.\]

References: - A157237 - Z.-W. Sun, "Mixed sums of primes and other terms", arXiv preprint arXiv:0901.3075 [math.NT], 2009.

Quoted from FormalConjectures/OEIS/157237.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 6 test statements, counted here but not shown.

`OeisA157237.conjecture`

Open: stated without proof.

On Feb. 24, 2009, Zhi-Wei Sun conjectured that $a(n) = 0$ if and only if $n < 16$ or $n \in \{18, 21, 24, 51, 84, 1011, 59586\}$; in other words, except for $35, 41, 47, 101, 167, 2021, 119171$, any odd integer greater than $30$ can be written as the sum of a prime congruent to $1 \bmod 6$, a positive power of $2$ and eleven times a positive power of $2$.

theorem conjecture (n : ℕ) (hn : 0 < n) :
    a n = 0 ↔ n ≤ 15 ∨ n = 18 ∨ n = 21 ∨ n = 24 ∨ n = 51 ∨ n = 84 ∨ n = 1011 ∨ n = 59586

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/157237.lean, line 79.

Sources

LeanOeisA157237.conjecture

TheoremSmallest $m$ such that $n^3 + m^3 + 1$ is prime #

$a(n)$ is the smallest natural number $m \ge 1$ such that $n^3 + m^3 + 1$ is prime.

References: - A159829

Quoted from FormalConjectures/OEIS/159829.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 1 open and 1 solved. It also has 4 test statements, counted here but not shown.

`OeisA159829.conjecture1`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a159829-conjecture1-counterexample/blob/6632e626baa7f28ad14045aa7408a84178ec128d/lean/A159829Conjecture1FC.lean#L52-L61.

Conjecture 1: For any $k \ge 3$, there are infinitely many primes of the form $n^k + m^k$ for $n, m \ge 1$. - Ulrich Krug, 2009

Answer: No. - Kenta Kitamura, 2026

theorem conjecture1 :
    ¬ ∀ (k : ℕ), 3 ≤ k →
      Set.Infinite {p : ℕ | ∃ n m : ℕ, 1 ≤ n ∧ 1 ≤ m ∧ p.Prime ∧
        p = n ^ k + m ^ k}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/159829.lean, line 99.

`OeisA159829.conjecture2`

Open: stated without proof.

Conjecture 2: For any $k \ge 3$, there are infinitely many primes of the form $n^k + m^k + 1$ for $n, m \ge 1$. - Ulrich Krug, 2009

theorem conjecture2 (k : ℕ) (hk : 3 ≤ k) :
    Set.Infinite {p : ℕ | ∃ n m : ℕ, 1 ≤ n ∧ 1 ≤ m ∧ p.Prime ∧ p = n ^ k + m ^ k + 1}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/159829.lean, line 111.

Sources

LeanOeisA159829.conjecture1 · OeisA159829.conjecture2

TheoremNumber of ways to express $n$ as sum of square, pentagonal, and hexagonal numbers #

\[a(n) = |\{(x, y, z) \in \mathbb{N}^3 : x^2 + p_5(y) + p_6(z) = n\}|\]

References: - A160324

Quoted from FormalConjectures/OEIS/160324.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 5 research or textbook statements: 5 open. It also has 4 test statements, counted here but not shown.

`OeisA160324.conjecture1`

Open: stated without proof.

In April 2009, Zhi-Wei Sun conjectured that $a(n) > 0$ for every $n = 0, 1, 2, 3, \dots$.

theorem conjecture1 (n : ℕ) : 0 < a n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/160324.lean, line 70.

`OeisA160324.conjecture2`

Open: stated without proof.

For each integer $m > 2$, any natural number $n$ can be written in the form $p_{m+1}(x_1) + \cdots + p_{2m}(x_m)$ with $x_1, \dots, x_m$ nonnegative integers, where $p_k(x) = (k-2)x(x-1)/2 + x$ ($x=0,1,2,\dots$) are $k$-gonal numbers. - Zhi-Wei Sun, Aug 15 2009

theorem conjecture2 (m : ℕ) (hm : m > 2) (n : ℕ) :
    ∃ x : Fin m → ℕ, n = ∑ i : Fin m, polygonalNumber (m + (i : ℕ) + 1) (x i)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/160324.lean, line 80.

`OeisA160324.conjecture3`

Open: stated without proof.

The sequence contains every positive integer. - Zhi-Wei Sun, Sep 04 2009

theorem conjecture3 (k : ℕ) (hk : 0 < k) : ∃ n : ℕ, a n = k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/160324.lean, line 89.

`OeisA160324.conjecture4`

Open: stated without proof.

Conjecture (Zhi-Wei Sun, Aug 21 2009): For any integer $m > 2$, each natural number $n$ can be expressed as $p_{m+1}(x_1) + p_{m+2}(x_2) + p_{m+3}(x_3) + r$ with $x_1, x_2, x_3 \in \mathbb{N}$ and $r \in \{0, \dots, m-3\}$.

theorem conjecture4 (m : ℕ) (hm : 2 < m) (n : ℕ) :
    ∃ x1 x2 x3 r : ℕ, r ≤ m - 3 ∧
      n = polygonalNumber (m + 1) x1 + polygonalNumber (m + 2) x2 + polygonalNumber (m + 3) x3 + r

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/160324.lean, line 99.

`OeisA160324.conjecture5`

Open: stated without proof.

Conjecture (Zhi-Wei Sun, Aug 21 2009): For each integer $m > 2$, all sufficiently large integers $n$ can be expressed in the form $p_{m+1}(x_1) + p_{m+2}(x_2) + p_{m+3}(x_3)$ with $x_1, x_2, x_3 \in \mathbb{N}$.

theorem conjecture5 (m : ℕ) (hm : 2 < m) :
    ∀ᶠ n in Filter.atTop,
      ∃ x1 x2 x3 : ℕ, n = polygonalNumber (m + 1) x1 + polygonalNumber (m + 2) x2 + polygonalNumber (m + 3) x3

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/160324.lean, line 110.

Sources

LeanOeisA160324.conjecture1 · OeisA160324.conjecture2 · OeisA160324.conjecture3 · OeisA160324.conjecture4 · OeisA160324.conjecture5

TheoremRowland-style prime-generating recurrence #

The sequence is defined by $a(1) = 2$ and for $n \ge 2$: $a(n) = a(n-1) + \gcd(n, a(n-1))$ if $n$ is even, and $a(n) = a(n-1) + \gcd(n-2, a(n-1))$ if $n$ is odd.

References: - A166944 - E. S. Rowland, "A natural prime-generating recurrence", J. Integer Sequences 11 (2008), Article 08.2.8. - V. Shevelev, "An infinite set of generators of primes based on the Rowland idea and conjectures concerning twin primes", arXiv preprint arXiv:0910.4676 [math.NT], 2009.

Quoted from FormalConjectures/OEIS/166944.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.

`OeisA166944.conjecture`

Open: stated without proof.

Conjecture: Every record of differences $a(n)-a(n-1)$ more than 5 is the greater of twin primes (A006512).

theorem conjecture (R : ℕ) (hR : 5 < R) (hrec : IsDifferenceRecord R) :
    IsGreaterTwinPrime R

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/166944.lean, line 85.

Sources

LeanOeisA166944.conjecture

TheoremChua's Euclidean prime sequence #

For a product $n$ of the preceding terms, Chua's sequence chooses the least prime dividing $d + n / d$ for some divisor $d$ of $n$. The open question is whether every prime occurs.

References: - OEIS A167604 - Andrew R. Booker, A variant of the Euclid--Mullin sequence containing every prime

Quoted from FormalConjectures/OEIS/167604.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.

`OeisA167604.conjecture`

Open: stated without proof.

Does Chua's sequence contain every prime?

theorem conjecture :
    ∀ p : ℕ, p.Prime → ∃ n ≥ 1, a n = p

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/167604.lean, line 75.

Sources

LeanOeisA167604.conjecture

TheoremSmallest index $k > n$ such that $(p_k+p_{k+1})/(p_n+p_{n+1})$ is an integer $\ge 2$#

References: - A167918

Quoted from FormalConjectures/OEIS/167918.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 open. It also has 5 test statements and 15 API statements, counted here but not shown.

`OeisA167918.conjecture_infinite`

Open: stated without proof.

Conjecture: the sequence is infinite, that is, for every $n \geq 1$ there is some $k > n$ with $S(n) \mid S(k)$, so that $a(n)$ is defined.

theorem conjecture_infinite (n : ℕ) (hn : n > 0) : ∃ k > n, S n ∣ S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/167918.lean, line 203.

`OeisA167918.conjecture1`

Open: stated without proof.

Conjecture: $f(n, k) = 2$ for infinitely many cases, where $k = a(n)$.

No hypothesis on the existence of $a(n)$ is needed: if no suitable $k > n$ exists then $a(n) = 0$ and $S(0) = 4 < 2 S(n)$, so such $n$ cannot be witnesses.

theorem conjecture1 (M : ℕ) :
    ∃ n : ℕ, n ≥ M ∧ n > 0 ∧ S (a n) = 2 * S n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/167918.lean, line 213.

`OeisA167918.conjecture2`

Open: stated without proof.

Open problem: is the ratio $f(n, k)$ bounded, where $k = a(n)$?

No hypothesis on the existence of $a(n)$ is needed: if no suitable $k > n$ exists then $a(n) = 0$ and $S(0) / S(n) = 4 / S(n) = 0$ for $n > 0$, so such $n$ do not affect boundedness. When $a(n) \neq 0$ we have $S(n) \mid S(a(n))$ by definition, so the division is exact.

theorem conjecture2 : ∃ C : ℕ, ∀ n : ℕ, n > 0 → S (a n) / S n ≤ C

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/167918.lean, line 225.

Sources

LeanOeisA167918.conjecture_infinite · OeisA167918.conjecture1 · OeisA167918.conjecture2

TheoremDenominators of $\sum_{k=1}^n \frac{1}{k 2^k}$#

$a(n)$ is the denominator of the sum

\[\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}\]

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

Quoted from FormalConjectures/OEIS/175386.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.

`OeisA175386.a_ne_one`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/175386.wip.lean#L304.

We conjecture that $\sum_{i=1}^{n} \frac{1}{i} \binom{2n-i-1}{i-1}$ is not an integer for $n > 1$.

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

theorem a_ne_one (n : ℕ) (hn : 1 < n) : a n ≠ 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/175386.lean, line 76.

Sources

LeanOeisA175386.a_ne_one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Determinants of 2 X 2 matrices… to Denominators of $\sum_{k=1}^n…

TheoremDeterminants of 2 X 2 matrices of non-overlapping blocks of 4 consecutive primes#

OeisA117027.conjecture

Sources

TheoremNumber of primes in \(n\)-th row of triangle \(k^2 - k + p_n\)#

OeisA117531.conjecture

Sources

TheoremLeast \(k\) such that cyclotomic polynomial \(\Phi_k(n)\) is prime#

OeisA117545.conjecture

Sources

TheoremSum of Fermat number and Mersenne number minus 1: \(2^{2^n} + 2^n - 1\)#

OeisA119563.conjecture

Sources

TheoremLeast \(k \ge 1\) such that \(2 \cdot n^k - 1\) is prime#

OeisA119591.conjecture

Sources

TheoremHalf-Fibonacci sequence#

OeisA120424.conjecture1

OeisA120424.conjecture2

Sources

TheoremRatio of product of GCDs to product of factorials of floor divisions#

OeisA129365.conjecture1

OeisA129365.conjecture2

OeisA129365.conjecture3

OeisA129365.conjecture4

Sources

TheoremOdious primes minus evil primes among first \(n\) primes#

OeisA130911.conjecture

Sources

TheoremRecurrence involving LCM: \(a(n) = x(n+1)/x(n) - 2\)#

OeisA135508.conjecture

Sources

TheoremNumber of Abelian cubes of length \(3n\) over an alphabet of size 3#

OeisA141057.conjecture1

OeisA141057.conjecture2

Sources

TheoremFactorial distance to nearest square#

OeisA145355.conjecture

Sources

TheoremCollatz step differences#

OeisA153330.conjecture1

OeisA153330.conjecture2

OeisA153330.conjecture3

OeisA153330.conjecture4

Sources

TheoremRepresentations as \(p + 2^x + 7 \cdot 2^y\) with \(p \equiv 5 \pmod 6\)#

OeisA157225.conjecture

Sources

TheoremRepresentations as \(p + 2^x + 11 \cdot 2^y\) with \(p \equiv 1 \pmod 6\)#

OeisA157237.conjecture

Sources

TheoremSmallest \(m\) such that \(n^3 + m^3 + 1\) is prime#

OeisA159829.conjecture1

OeisA159829.conjecture2

Sources

TheoremNumber of ways to express \(n\) as sum of square, pentagonal, and hexagonal numbers#

OeisA160324.conjecture1

OeisA160324.conjecture2

OeisA160324.conjecture3

OeisA160324.conjecture4

OeisA160324.conjecture5

Sources

TheoremRowland-style prime-generating recurrence#

OeisA166944.conjecture

Sources

TheoremChua's Euclidean prime sequence#

OeisA167604.conjecture

Sources

TheoremSmallest index \(k > n\) such that \((p_k+p_{k+1})/(p_n+p_{n+1})\) is an integer \(\ge 2\)#

OeisA167918.conjecture_infinite

OeisA167918.conjecture1

OeisA167918.conjecture2

Sources

TheoremDenominators of \(\sum_{k=1}^n \frac{1}{k 2^k}\)#

OeisA175386.a_ne_one

Sources

TheoremDeterminants of 2 X 2 matrices of non-overlapping blocks of 4 consecutive primes #

`OeisA117027.conjecture`

`OeisA117531.conjecture`

TheoremLeast \(k\) such that cyclotomic polynomial \(\Phi_k(n)\) is prime #

`OeisA117545.conjecture`

`OeisA119563.conjecture`

TheoremLeast \(k \ge 1\) such that \(2 \cdot n^k - 1\) is prime #

`OeisA119591.conjecture`

TheoremHalf-Fibonacci sequence #

`OeisA120424.conjecture1`

`OeisA120424.conjecture2`

TheoremRatio of product of GCDs to product of factorials of floor divisions #

`OeisA129365.conjecture1`

`OeisA129365.conjecture2`

`OeisA129365.conjecture3`

`OeisA129365.conjecture4`

TheoremOdious primes minus evil primes among first \(n\) primes #

`OeisA130911.conjecture`

`OeisA135508.conjecture`

TheoremNumber of Abelian cubes of length \(3n\) over an alphabet of size 3 #

`OeisA141057.conjecture1`

`OeisA141057.conjecture2`

TheoremFactorial distance to nearest square #

`OeisA145355.conjecture`

TheoremCollatz step differences #

`OeisA153330.conjecture1`

`OeisA153330.conjecture2`

`OeisA153330.conjecture3`

`OeisA153330.conjecture4`

`OeisA157225.conjecture`

`OeisA157237.conjecture`

TheoremSmallest \(m\) such that \(n^3 + m^3 + 1\) is prime #

`OeisA159829.conjecture1`

`OeisA159829.conjecture2`

TheoremNumber of ways to express \(n\) as sum of square, pentagonal, and hexagonal numbers #

`OeisA160324.conjecture1`

`OeisA160324.conjecture2`

`OeisA160324.conjecture3`

`OeisA160324.conjecture4`

`OeisA160324.conjecture5`

TheoremRowland-style prime-generating recurrence #

`OeisA166944.conjecture`

TheoremChua's Euclidean prime sequence #

`OeisA167604.conjecture`

`OeisA167918.conjecture_infinite`

`OeisA167918.conjecture1`

`OeisA167918.conjecture2`

`OeisA175386.a_ne_one`