Sequence related to NOR… to $a(n) = \sum_{j=1}^{n} (3^j +…

\[a(n) = \sum_{j=0}^{n-1} (-1)^j \binom{2j}{j} \binom{2n-j-2}{n-j-1}\]

References: - A112521

Quoted from FormalConjectures/OEIS/112521.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.

`OeisA112521.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a112521-formal-conjectures/blob/d4ee80e997c20209a1f18b7b9aa3521150d5474d/lean/OeisA112521Proof.lean#L876-L885.

Conjecture: Starting with $n=1$, $a(n)$ is the main diagonal of the array $T(n, k)$.

theorem conjecture : ∀ (n : ℕ), n ≥ 1 → (a n : ℤ) = T n n

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

Sources

LeanOeisA112521.conjecture

TheoremA generalized Stern sequence #

A112970: A generalized Stern sequence, defined by the recurrence relations: $a(2n+1) = a(n)$ and $a(2n) = a(n) + a(n-2)$ with $a(0)=1$, $a(1)=1$ and $a(n)=0$ for $n \le -1$.

References: - A112970

Quoted from FormalConjectures/OEIS/112970.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.

`OeisA112970.conjecture1`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a112970-formal-conjectures/blob/71ae72f443bd9bee7d958f0a19d9f9ec5ab82af5/lean/OeisA112970FC.lean#L43-L46.

Conjecture: $a(2^n)=a(2^(n+1)+1)=\textrm{A033638}(n)$. This formalizes the equality $a(2^n) = a(2^(n+1)+1)$.

theorem conjecture1 (n : ℕ) : a (2^n) = a (2^(n + 1) + 1)

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

`OeisA112970.conjecture1_value`

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA112970_conjecture1_value.lean#L139.

Second part of the conjecture, $a(2^n)=\textrm{A033638}(n)=\lfloor n^2 / 4 \rfloor + 1$. It holds by induction on $n$, since $a(2^{n+1}) = a(2^n) + a(2^n - 2)$ for $n \ge 1$ and $a(2^m - 2) = \lfloor (m+1)/2 \rfloor$ for $m \ge 1$.

theorem conjecture1_value (n : ℕ) : a (2^n) = n ^ 2 / 4 + 1

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

`OeisA112970.conjecture2`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a112970-formal-conjectures/blob/71ae72f443bd9bee7d958f0a19d9f9ec5ab82af5/lean/OeisA112970FC.lean#L56-L64.

Conjecture: $a(2^n-1)=a(3*2^n-1)=1$. This formalizes the equality part $a(2^n-1) = a(3*2^n-1)$.

theorem conjecture2 (n : ℕ) : a (2^n - 1) = a (3 * 2^n - 1)

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

`OeisA112970.conjecture3`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a112970-formal-conjectures/blob/71ae72f443bd9bee7d958f0a19d9f9ec5ab82af5/lean/OeisA112970FC.lean#L48-L54.

Conjecture: $a(2^n-1)=a(3*2^n-1)=1$. This formalizes the value part $a(2^n-1)=1$.

theorem conjecture3 (n : ℕ) : a (2^n - 1) = 1

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

Sources

LeanOeisA112970.conjecture1 · OeisA112970.conjecture1_value · OeisA112970.conjecture2 · OeisA112970.conjecture3

TheoremNumber of digits of n raised to the power of the sum of the digits of n #

References: - A113010

Quoted from FormalConjectures/OEIS/113010.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.

`OeisA113010.conjecture`

Open: stated without proof.

$n=1$ and $32$ are two fixed points. Are there any others?

theorem conjecture : ∃ n : ℕ, a n = n ∧ n ≠ 1 ∧ n ≠ 32

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

Sources

LeanOeisA113010.conjecture

TheoremNumber of digits of n raised to the power of the digital root of n #

References: - A113019

Quoted from FormalConjectures/OEIS/113019.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.

`OeisA113019.conjecture`

Proved here.

$n=1$ and $32$ are fixed points. Are there any others?

Yes: 9^9 = 387420489 is also a fixed point. - Kenta Kitamura, Aug 14 2026

theorem conjecture : ¬ ∀ n : ℕ, a n = n → n = 1 ∨ n = 32

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

Sources

LeanOeisA113019.conjecture

TheoremSmallest number $m$ such that $2^n - m$ and $2^n + m$ are primes #

References: - A113213

Quoted from FormalConjectures/OEIS/113213.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.

`OeisA113213.conjecture`

Open: stated without proof.

Conjecture: $a(n) = O(n^3)$.

The source defines $a(n)$ as the least $m$ with $2^n - m$ and $2^n + m$ prime, so it implicitly asserts that such an $m$ exists. Since a n = 0 when no such $m$ exists, the existence of a prime pair is stated explicitly for all sufficiently large $n$.

theorem conjecture :
    (∀ᶠ n : ℕ in Filter.atTop, ∃ m, (2 ^ n - m).Prime ∧ (2 ^ n + m).Prime) ∧
    (fun n : ℕ => (a n : ℝ)) =O[Filter.atTop] (fun n : ℕ => (n ^ 3 : ℝ))

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

Sources

LeanOeisA113213.conjecture

TheoremExpansion of g.f. $-(1 - 48x^2 - 256x^3) / ((1 - 4x)(1 + 4x)(1 + 4x + 16x^2))$#

Corresponds to m = 4 in a family of 4th-order linear recurrence sequences

This sequence is defined by the linear recurrence relation with signature $(-4, 0, 64, 256)$ and initial values $a(0) = -1, a(1) = 4, a(2) = 32, a(3) = 64$. The recurrence is $a(n) = -4 a(n-1) + 64 a(n-3) + 256 a(n-4)$.

References: - A113250

Quoted from FormalConjectures/OEIS/113250.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.

`OeisA113250.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a113249-family-square-terms-lean/blob/9b999db08344184285e8050c2722c845fd5f5309/lean/OeisA113249FamilyFC.lean#L106-L114.

Conjecture: $a(m, 2n+1)$ is a perfect square for all $m$ (see A113249). Specialized to $m = 4$, which is A113250.

theorem conjecture : ∀ n : ℕ, IsSquare (a (2 * n + 1))

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

Sources

LeanOeisA113250.conjecture

TheoremConjectures associated with A113252 #

Corresponds to m = 6 in a family of 4th order linear recurrence sequences

This sequence is defined by the linear recurrence relation a(n) = -4 a(n-1) + 144 a(n-3) + 1296 a(n-4) for n > 3. Initial values are a(0) = -1, a(1) = 4, a(2) = 92, a(3) = 784.

References: - A113252

Quoted from FormalConjectures/OEIS/113252.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.

`OeisA113252.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a113249-family-square-terms-lean/blob/9b999db08344184285e8050c2722c845fd5f5309/lean/OeisA113249FamilyFC.lean#L116-L124.

Conjecture: $a(m, 2n+1)$ is a perfect square for all $m, n$ (see A113249). Specialized for $m=6$, which is A113252.

theorem conjecture : ∀ n : ℕ, IsSquare (a (2 * n + 1))

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

Sources

LeanOeisA113252.conjecture

TheoremSquare odd-indexed terms in the recurrence $a(n) = 8a(n-1) - 8a(n-2) + 8a(n-3) - a(n-4)$#

A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences.

The sequence $a(n)$ is defined by the initial conditions $a(0)=-1, a(1)=4, a(2)=176, a(3)=3136$, and the linear recurrence relation $a(n) = -4 * a (n-1) + 256 * a (n-3) + 4096 * a (n-4)$ for $n \ge 4$.

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

Quoted from FormalConjectures/OEIS/113254.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.

`OeisA113254.a_odd_is_square`

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

Conjecture: $a(8, 2n+1)$ is a perfect square for all $n$ (see A113249).

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

theorem a_odd_is_square : ∀ n : ℕ, IsSquare (a (2 * n + 1))

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

Sources

LeanOeisA113254.a_odd_is_square

TheoremConjectures associated with A113255 #

Corresponds to m = 9 in a family of 4th-order linear recurrence sequences

This sequence is defined by the recurrence relation $a(n) = -4 a(n-1) + 324 a(n-3) + 6561 a(n-4)$ for n > 3. Initial values are $a(0) = -1, a(1) = 4, a(2) = 227, a(3) = 5329$.

References: - A113255

Quoted from FormalConjectures/OEIS/113255.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.

`OeisA113255.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a113249-family-square-terms-lean/blob/9b999db08344184285e8050c2722c845fd5f5309/lean/OeisA113249FamilyFC.lean#L126-L134.

Conjecture: $a(m, 2n+1)$ is a perfect square for all $m, n$ (see A113249). Specialized for $m=9$, which is A113255.

theorem conjecture : ∀ n : ℕ, IsSquare (a (2 * n + 1))

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

Sources

LeanOeisA113255.conjecture

TheoremAscending descending base exponent transform of squares #

a n is $\sum_{i=1}^n (i^2)^((n-i+1)^2)$.

References: - A113257

Quoted from FormalConjectures/OEIS/113257.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.

`OeisA113257.conjecture1`

Open: stated without proof.

The smallest prime in this sequence is $a(2) = 5$. What is the next prime?

theorem conjecture1 :
    conjecture1.answer = a (sInf {n : ℕ | 2 < n ∧ (a n).Prime})

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

`OeisA113257.conjecture2`

Open: stated without proof.

What is the first square value after 1?

theorem conjecture2 :
    conjecture2.answer = a (sInf {n : ℕ | 1 < n ∧ IsSquare (a n)})

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

Sources

LeanOeisA113257.conjecture1 · OeisA113257.conjecture2

TheoremAscending descending base exponent transform of factorials #

References: - A113258

Quoted from FormalConjectures/OEIS/113258.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.

`OeisA113258.conjecture`

Open: stated without proof.

Is there a nontrivial power after $a(4) = 5^3$?

theorem conjecture :
  ∃ n > 4, ∃ b > 1, ∃ e > 1, a n = b ^ e

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

Sources

LeanOeisA113258.conjecture

TheoremAscending descending base exponent transform of $2^n$#

References: - A113271

Quoted from FormalConjectures/OEIS/113271.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 8 test statements, counted here but not shown.

`OeisA113271.conjecture1`

Open: stated without proof.

The first prime terms in this (always odd) sequence are $a(1) = 3$, $a(3) = 41$, and $a(4) = 593$. What is the next prime?

The OEIS comment currently says $a(5) = 543$ , but this conflicts with its defining formula, b-file, and examples: the actual index-five term is the composite number 135457. Consequently the search for the next prime must begin after index 4, not after index 5.

theorem conjecture1 :
  conjecture1.answer = a (sInf {n : ℕ | 4 < n ∧ (a n).Prime})

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

Sources

LeanOeisA113271.conjecture1

TheoremNumber of prime powers $q<=n$ such that also $q+2$ is a prime power #

References: - A113609

Quoted from FormalConjectures/OEIS/113609.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.

`OeisA113609.conjecture`

Open: stated without proof.

(25,27) is the smallest pair of prime powers (q,q+2) such that both q and q+2 are not primes, conjecture: there are more (but not < 10^6).

theorem conjecture :
  ∃ q ≥ 1000000,
    IsOeisPrimePower q ∧ IsOeisPrimePower (q + 2) ∧
    ¬ q.Prime ∧ ¬ (q + 2).Prime

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

Sources

LeanOeisA113609.conjecture

TheoremDifference between first odd semiprime $> 2^n$ and $2^n$#

References: - A114137

Quoted from FormalConjectures/OEIS/114137.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 and 1 API statement, counted here but not shown.

`OeisA114137.conjecture1`

Open: stated without proof.

In this powers of 2 sequence, does 1 occur infinitely often?

theorem conjecture1 :
  Set.Infinite {n : ℕ | a n = 1}

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

`OeisA114137.conjecture2`

Open: stated without proof.

Does every odd number occur?

theorem conjecture2 :
  ∀ k : ℕ, Odd k → ∃ n : ℕ, a n = k

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

Sources

LeanOeisA114137.conjecture1 · OeisA114137.conjecture2

TheoremLargest odd divisor of $a(n-1) + \textrm{prime}(n)$#

$a(0)=0$; thereafter $a(n)$ = largest odd divisor of $a(n-1) + \textrm{prime}(n)$.

References: - A114216

Quoted from FormalConjectures/OEIS/114216.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.

`OeisA114216.conjecture`

Open: stated without proof.

Is $a(33900)$ the last term equal to $1$?

theorem conjecture :
  ∀ n > 33900, a n ≠ 1

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

Sources

LeanOeisA114216.conjecture

TheoremNumerator of $\zeta(4n)/\zeta(2n)^2$ (with $a(0)=2$ instead of $-2$)#

The ratio $\zeta(4n)/\zeta(2n)^2$ for $n \ge 1$ is the rational number

\[ Q_n = -2 \frac{B_{4n}}{B_{2n}^2 \binom{4n}{2n}} \]

where $B_k$ is the $k$-th Bernoulli number. The sequence $a(n)$ is the numerator of $Q_n$, with $a(0)$ defined as $2$.

References: - A114362

Quoted from FormalConjectures/OEIS/114362.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.

`OeisA114362.conjecture1`

Open: stated without proof.

Conjecture: if an integer $n > 1$ is odd, then $\zeta(2n)/\zeta(n)^2$ is irrational. Cf. W. Kohnen (link) and my conjecture in A348829. - Thomas Ordowski, Jan 05 2022

theorem conjecture1 (n : ℕ) (hn_gt_one : 1 < n) (hn_odd : Odd n) :
    Irrational ((riemannZeta (2 * n : ℂ) / (riemannZeta (n : ℂ)) ^ 2).re)

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

`OeisA114362.conjecture2`

Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/872759d0b464254d868f107fe7f9cf762900f57d/FormalConjectures/OEIS/114362.lean#L646.

Conjecture: $\frac{1 - t(n)}{1 + t(n)} = \frac{1}{2^n} + \frac{1}{3^n} + \frac{1}{5^n} + \frac{1}{7^n} + O(\frac{1}{11^n})$, where $t(n) = \zeta(2n)/\zeta(n)^2$. Cf. A348829. - Thomas Ordowski, Nov 13 2022

theorem conjecture2 :
    (fun n : ℕ => (1 - t n) / (1 + t n) -
      (1 / (2:ℝ)^n + 1 / (3:ℝ)^n + 1 / (5:ℝ)^n + 1 / (7:ℝ)^n))
      =O[atTop] (fun n : ℕ => 1 / (11:ℝ)^n)

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

Sources

LeanOeisA114362.conjecture1 · OeisA114362.conjecture2

TheoremEach term is previous term plus floor of harmonic mean of two previous terms.#

$a(1) = 1, a(2) = 2$ and $a(n) = a(n-1) + \lfloor \frac{2 a(n-1) a(n-2)}{a(n-1) + a(n-2)} \rfloor$ for $n \ge 3$.

References: - A114831

Quoted from FormalConjectures/OEIS/114831.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 4 test statements, counted here but not shown.

`OeisA114831.conjecture3`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a114831-asymptotic/blob/54cdeeed2ef5838e3aa61a3a228e6867802d20df/lean/OeisA114831FC.lean#L252-L285.

Conjecture based on OEIS A114831: What is this sequence, asymptotically? If the limit exists, the ratio of consecutive terms must tend to $\sqrt{3}$:

\[ \lim_{n \to \infty} \frac{a(n+1)}{a(n)} = \sqrt{3}. \]

That's because $a(n)$ is positive, monotonically increasing ($a(n) > a(n-1)$) and $a(n+2) \geq a(n+1) + a(n)$. So $a(n)$ grows exponentially, at least as fast as the Fibonnaci numbers. Assuming $\frac{a(n+1)}{a(n)}$ tend to a limit L, solving for L in the definition of $a(n)$ gives $L=\sqrt{3}$.

theorem conjecture3 :
    Tendsto (fun n ↦ (a (n + 1) : ℝ) / (a n : ℝ)) atTop (nhds (Real.sqrt 3))

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

Sources

LeanOeisA114831.conjecture3

TheoremPartial sums of $\binom{2n}{n}^2$#

\[a(n) = \sum_{k=0}^n \binom{2k}{k}^2\]

References: - A115257

Quoted from FormalConjectures/OEIS/115257.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.

`OeisA115257.conjecture`

Open: stated without proof.

Conjecture: For any positive integer n, the polynomials Sum_{k=0}^n binomial(2k,k)^2x^k and Sum_{k=0}^n binomial(2k,k)^2x^k/(k+1) are irreducible over the field of rational numbers. - Zhi-Wei Sun, Mar 23 2013

theorem conjecture :
  ∀ (n : ℕ), 1 ≤ n → Irreducible (polyP n) ∧ Irreducible (polyQ n)

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

Sources

LeanOeisA115257.conjecture

Theorem$a(n)$ = the number of values of $k <= 10^n$ such that $\sqrt{k(k+1)(k+2)(k+3)+1}$ is prime #

Since $\sqrt{k(k+1)(k+2)(k+3)+1} = k^2 + 3k + 1$, $a(n) = \#\{k \in \mathbb{N} \mid 1 \le k \le 10^n \land (k^2 + 3k + 1) \text{ is prime} \}.$

References: - A115366

Quoted from FormalConjectures/OEIS/115366.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.

`OeisA115366.conjecture`

Open: stated without proof.

Conjecture: $a(n)/A006880(n) \rightarrow 1.77...$ where A006880(n) is the number of primes $\le 10^n$.

theorem conjecture :
    ∃ L : ℝ,
      Tendsto (fun n : ℕ => (a n : ℝ) / (Nat.primeCounting' (10 ^ n) : ℝ)) atTop (nhds L) ∧
      1.77 ≤ L ∧ L ≤ 1.78

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

Sources

LeanOeisA115366.conjecture

Theorem$a(n) = \sum_{j=1}^{n} (3^j + (-2)^j)$#

References: - A116150

Quoted from FormalConjectures/OEIS/116150.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.

`OeisA116150.conjecture`

Open: stated without proof.

First primes are $a(11) = 264353$ and $a(17) = 193622861$. Additional primes: $a(71)$, $a(91)$, $a(431)$. What is the next prime?

theorem conjecture : conjecture.answer = a (sInf {n : ℕ | 431 < n ∧ (a n).Prime})

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

Sources

LeanOeisA116150.conjecture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Sequence related to NOR… to $a(n) = \sum_{j=1}^{n} (3^j +…

TheoremSequence related to NOR bracketings#

OeisA112521.conjecture

Sources

TheoremA generalized Stern sequence#

OeisA112970.conjecture1

OeisA112970.conjecture1_value

OeisA112970.conjecture2

OeisA112970.conjecture3

Sources

TheoremNumber of digits of n raised to the power of the sum of the digits of n#

OeisA113010.conjecture

Sources

TheoremNumber of digits of n raised to the power of the digital root of n#

OeisA113019.conjecture

Sources

TheoremSmallest number \(m\) such that \(2^n - m\) and \(2^n + m\) are primes#

OeisA113213.conjecture

Sources

TheoremExpansion of g.f. \(-(1 - 48x^2 - 256x^3) / ((1 - 4x)(1 + 4x)(1 + 4x + 16x^2))\)#

OeisA113250.conjecture

Sources

TheoremConjectures associated with A113252#

OeisA113252.conjecture

Sources

TheoremSquare odd-indexed terms in the recurrence \(a(n) = 8a(n-1) - 8a(n-2) + 8a(n-3) - a(n-4)\)#

OeisA113254.a_odd_is_square

Sources

TheoremConjectures associated with A113255#

OeisA113255.conjecture

Sources

TheoremAscending descending base exponent transform of squares#

OeisA113257.conjecture1

OeisA113257.conjecture2

Sources

TheoremAscending descending base exponent transform of factorials#

OeisA113258.conjecture

Sources

TheoremAscending descending base exponent transform of \(2^n\)#

OeisA113271.conjecture1

Sources

TheoremNumber of prime powers \(q<=n\) such that also \(q+2\) is a prime power#

OeisA113609.conjecture

Sources

TheoremDifference between first odd semiprime \(> 2^n\) and \(2^n\)#

OeisA114137.conjecture1

OeisA114137.conjecture2

Sources

TheoremLargest odd divisor of \(a(n-1) + \textrm{prime}(n)\)#

OeisA114216.conjecture

Sources

TheoremNumerator of \(\zeta(4n)/\zeta(2n)^2\) (with \(a(0)=2\) instead of \(-2\))#

OeisA114362.conjecture1

OeisA114362.conjecture2

Sources

TheoremEach term is previous term plus floor of harmonic mean of two previous terms.#

OeisA114831.conjecture3

Sources

TheoremPartial sums of \(\binom{2n}{n}^2\)#

OeisA115257.conjecture

Sources

Theorem\(a(n)\) = the number of values of \(k <= 10^n\) such that \(\sqrt{k(k+1)(k+2)(k+3)+1}\) is prime#

OeisA115366.conjecture

Sources

Theorem\(a(n) = \sum_{j=1}^{n} (3^j + (-2)^j)\)#

OeisA116150.conjecture

Sources

TheoremSequence related to NOR bracketings #

`OeisA112521.conjecture`

TheoremA generalized Stern sequence #

`OeisA112970.conjecture1`

`OeisA112970.conjecture1_value`

`OeisA112970.conjecture2`

`OeisA112970.conjecture3`

TheoremNumber of digits of n raised to the power of the sum of the digits of n #

`OeisA113010.conjecture`

TheoremNumber of digits of n raised to the power of the digital root of n #

`OeisA113019.conjecture`

TheoremSmallest number \(m\) such that \(2^n - m\) and \(2^n + m\) are primes #

`OeisA113213.conjecture`

`OeisA113250.conjecture`

TheoremConjectures associated with A113252 #

`OeisA113252.conjecture`

`OeisA113254.a_odd_is_square`

TheoremConjectures associated with A113255 #

`OeisA113255.conjecture`

TheoremAscending descending base exponent transform of squares #

`OeisA113257.conjecture1`

`OeisA113257.conjecture2`

TheoremAscending descending base exponent transform of factorials #

`OeisA113258.conjecture`

`OeisA113271.conjecture1`

TheoremNumber of prime powers \(q<=n\) such that also \(q+2\) is a prime power #

`OeisA113609.conjecture`

`OeisA114137.conjecture1`

`OeisA114137.conjecture2`

`OeisA114216.conjecture`

`OeisA114362.conjecture1`

`OeisA114362.conjecture2`

`OeisA114831.conjecture3`

`OeisA115257.conjecture`

Theorem\(a(n)\) = the number of values of \(k <= 10^n\) such that \(\sqrt{k(k+1)(k+2)(k+3)+1}\) is prime #

`OeisA115366.conjecture`

`OeisA116150.conjecture`