Pentanacci $\pi$ sequence to $a(n) = \sum_{i=0}^n…

TheoremPentanacci $\pi$ sequence #

Start with $a(1)=a(2)=a(3)=a(4)=a(5)=1$ and for $n>5$, $a(n) = \pi(\sum_{j=1}^5 a(n-j))$ where $\pi = A000720$.

References: - A100478

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

`OeisA100478.conjecture`

Solved: stated here without proof.

Starting with other values of $a(1)$, $a(2)$, $a(3)$, $a(4)$, $a(5)$ what behaviors are possible? Does the sequence always stick at a single integer after some point, or can it go into a loop, or is there a third pattern?

KitaKen1 showed the sequence either becomes constant or goes into a loop, see https://github.com/KitaKen1/oeis-a100478-eventual-periodicity/blob/642eed0ffee26415528ab8c48c5181826be04860/lean/OeisA100478FC.lean#L158-L168.

tadamcz showed the sequence always becomes constant, see https://tadamcz.com/fc-review-results/aea251bb26/#/f/OEIS/100478.

theorem conjecture:
  ∀ v : Fin 5 → ℕ, (∀ i, 0 < v i) → ∃ c ∈ ({66, 67, 68, 70, 71, 72} : Finset ℕ),
  ∀ᶠ n in Filter.atTop, aGeneral v n = c

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

Sources

LeanOeisA100478.conjecture

TheoremConjectures associated with A100800 #

Let $f(n) = n + \text{sum of the digits of } n$. If $f(n)$ is multiple of $n$ then $a(n)= f(n)$ else $a(n) = f(f(f(n)))\dots$ until one gets a multiple of $n$; $a(n) = 0$ if no such number exists.

References: - A100800

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

`OeisA100800.conjecture`

Open: stated without proof.

A100800 Conjecture: No term is zero.

theorem conjecture : ∀ (n : ℕ), n ≠ 0 → a n ≠ 0

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

Sources

LeanOeisA100800.conjecture

TheoremConjectures associated with A101779 #

$a(n)$ is the least $k$ such that all of $k, 2k+1, 3k+2, ..., nk+n-1$ are primes, or $0$ if no such $k$ is found. It is conjectured $k$ always exists.

References: - A101779

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

`OeisA101779.conjecture`

Open: stated without proof.

It is conjectured k always exists.

theorem conjecture : ∀ (n : ℕ), 1 ≤ n → ∃ k : ℕ, Ak n k

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

Sources

LeanOeisA101779.conjecture

TheoremConjectures associated with A102371 #

The sequence $a(n)$ is defined by the recurrence relation $a(1)=1$, and for $n>1$, $a(n) = a(n-1) \operatorname{XOR} (a(n-1) + n)$. The conjecture asks if $a(n) = 2^n - 1 - \operatorname{A105033}(n-1)$ for $n \ge 1$.

References: - A102371

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

`OeisA102371.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a102371/blob/d80fba9/lean/OeisA102371FC.lean#L490-L497.

Do we have $a(n) = 2^n - 1 - \operatorname{A105033}(n-1)$ for $n \ge 1$?

Note: The OEIS comment suggests $n-1$ which means this applies at least for $n \ge 1$, as we assume $\operatorname{A105033}(\mathbb{N})$ is defined on $\mathbb{N}$. We include the case $n=1$ which relies on $A105033(0)$, which is 0.

theorem conjecture : ∀ n : ℕ, 0 < n → a n = 2^n - 1 - OeisA105033.a (n - 1)

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

Sources

LeanOeisA102371.conjecture

TheoremFloor of sum of $\{n/k\}$#

Given $n$, sum all division remainders $\{n/k\}$, with $k=1,\dots,n$. The value $a(n)$ is given by the floor of that sum. Note that $\{x\}:=x-[x]$. Conjecture: a(n) ~ (1-EulerGamma)n.

References: - A102722

Quoted from FormalConjectures/OEIS/102722.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 and 5 API statements, counted here but not shown.

`OeisA102722.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-102722-asymptotic/blob/0e3bf1bc6dfd04627f926b07fb8d25f4395a5072/lean/OEIS102722FC.lean#L18-L24.

A102722 Conjecture: $a(n) \sim (1-\gamma)n$.

theorem conjecture :
    (fun n : ℕ => (a n : ℝ)) ~[atTop]
      (fun n : ℕ => (1 - Real.eulerMascheroniConstant) * (n : ℝ))

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

Sources

LeanOeisA102722.conjecture

Theorem$a(0) = 1$, $a(n) = a(n-1)a(n-1) + 2$#

References: - A102847

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

`OeisA102847.conjecture`

Open: stated without proof.

Prime for $a(1) = 3$, $a(2) = 11$, $a(4) = 15131$; semiprime for $a(3) = 123 = 3 * 41$, $a(5) = 228947163 = 3 * 76315721$. $a(6)$, added by Jonathan Vos Post, has 4 prime factors. $a(7) = 41 * 811^2 * 106693969 * 317171188688357726699 * 8272236925540996054440172449761$. When is the next prime in the sequence?

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

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

Sources

LeanOeisA102847.conjecture

TheoremNumber of decompositions of $2n+1$ into $2p+q$, where $p$ and $q$ are both odd primes #

References: - A103151

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

`OeisA103151.conjecture`

Open: stated without proof.

Conjecture: all items for $n \ge 4$ are greater than or equal to $1$. This is a stronger conjecture than the Goldbach conjecture.

theorem conjecture (n : ℕ) (hn : n ≥ 4) : a n ≥ 1

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

Sources

LeanOeisA103151.conjecture

TheoremFibonacci transform satisfying $|a(n)| = F(n+1)$#

The sequence $a(n)$ satisfies the linear recurrence relation:

\[a(n) = 3a(n-1) - 4a(n-2) + 2a(n-3) - a(n-4)\]

with initial terms $a(0)=0, a(1)=1, a(2)=1, a(3)=0$. The sequence takes values in $\mathbb{Z}$.

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

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

`OeisA103311.a_abs_eq_fib`

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

Fibonacci transform satisfying $|a(n)| = F(n+1)$.

Conjecture: all elements in absolute value are Fibonacci numbers.

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

theorem a_abs_eq_fib (n : ℕ) : ∃ m : ℕ, Int.natAbs (a n) = Nat.fib m

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

Sources

LeanOeisA103311.a_abs_eq_fib

Theorem$a(n) = 3a(n-1) + a(n-2) - 3a(n-3)$#

References: - A103425

Quoted from FormalConjectures/OEIS/103425.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 solved. It also has 5 test statements, counted here but not shown.

`OeisA103425.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a103425-prime-free/blob/b04b155/lean/OeisA103425FC.lean#L13-L35.

The current sequence contains primes, including $3, 5, 41, 21523361$. Is there an $(a, b, c)$ weighted tribonacci sequence with $a, b, c$ relatively prime which is prime-free?

Yes: take $(a, b, c) = (1, 1, -1)$ and the constant sequence $x(n) = 4$. The linked Lean proof is by Kenta Kitamura.

theorem conjecture :
    ∃ (a b c : ℤ) (x : ℕ → ℤ),
      Nat.gcd (Int.gcd a b) c.natAbs = 1 ∧
      IsWeightedTribonacci a b c x ∧
      ∀ n, ¬ (x n).natAbs.Prime

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

`OeisA103425.conjecture.variants.nonconstant`

Proved here.

Is there a non-constant $(a, b, c)$ weighted tribonacci sequence with $a, b, c$ relatively prime which is prime-free?

Yes: take $(a, b, c) = (1, 1, -1)$ and $x(n) = 4(n + 1)$.

theorem conjecture.variants.nonconstant :
    ∃ (a b c : ℤ) (x : ℕ → ℤ),
      Nat.gcd (Int.gcd a b) c.natAbs = 1 ∧
      IsWeightedTribonacci a b c x ∧
      (∃ m n, x m ≠ x n) ∧
      ∀ n, ¬ (x n).natAbs.Prime

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

`OeisA103425.conjecture.variants.nonconstant_distinct_coeffs`

Proved here.

Is there a non-constant $(a, b, c)$ weighted tribonacci sequence with $a, b, c$ relatively prime and pairwise distinct which is prime-free?

Yes: take $(a, b, c) = (3, -3, 1)$ and $x(n) = (n + 2)^2$.

theorem conjecture.variants.nonconstant_distinct_coeffs :
    ∃ (a b c : ℤ) (x : ℕ → ℤ),
      Nat.gcd (Int.gcd a b) c.natAbs = 1 ∧
      a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
      IsWeightedTribonacci a b c x ∧
      (∃ m n, x m ≠ x n) ∧
      ∀ n, ¬ (x n).natAbs.Prime

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

Sources

LeanOeisA103425.conjecture · OeisA103425.conjecture.variants.nonconstant · OeisA103425.conjecture.variants.nonconstant_distinct_coeffs

TheoremSmallest power with base>1 and exponent $n$ without digit 0 #

For statistical reasons it is conjectured that the sequence is finite. Also it is conjectured that $a(40)$ does not exist (i.e. the sequence is empty for $n=40$).

References: - A103662

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

`OeisA103662.conjecture`

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

For statistical reasons it is conjectured that the sequence is finite. Finite means here that for some $n$, no power $b^n$ with base $b > 1$ has a zeroless decimal representation, which in our definition results in $a(n) = 0$.

This holds for $n = 2500$ (source). Take any integer $b > 1$ and let $N = b^{2500}$. Since $b \ge 2$, we have $N \ge 2^{2500} > 10^5$, so $N$ has at least six decimal digits. We split into four cases depending on the divisibility of $b$ by $2$ and $5$:

If $10 \mid b$: Then $10 \mid N$, so the units digit of $N$ is $0$.

If $b$ is odd and $5 \nmid b$: Since $b$ is odd and the Carmichael function satisfies $\lambda(16) = 4 \mid 2500$, we have $N \equiv 1 \pmod{16}$. Since $5 \nmid b$ and $\varphi(5^5) = 2500$, Euler's totient theorem gives $N \equiv 1 \pmod{3125}$. By the Chinese Remainder Theorem, $N \equiv 1 \pmod{50000}$ (as $16 \cdot 3125 = 50000$), so the tens digit of $N$ is $0$.

If $b$ is odd and $5 \mid b$: As above, $N \equiv 1 \pmod{16}$. Since $5 \mid b$ and $2500 \ge 4$, we also have $5^4 = 625 \mid N$, so $N \equiv 0 \pmod{625}$. Since $16 \cdot 625 = 10^4$ and $625 \equiv 1 \pmod{16}$, the Chinese Remainder Theorem gives $N \equiv 625 \pmod{10^4}$. Because $N > 10^4$, the last four digits of $N$ are $0625$, so its thousands digit is $0$.

If $b$ is even and $5 \nmid b$: Since $2 \mid b$ and $2500 \ge 5$, we have $2^5 = 32 \mid N$, so $N \equiv 0 \pmod{32}$. Since $5 \nmid b$, Euler's theorem again gives $N \equiv 1 \pmod{3125}$. Because $32 \cdot 3125 = 10^5$ and $9376 = 293 \cdot 32 = 3 \cdot 3125 + 1$, the Chinese Remainder Theorem gives $N \equiv 9376 \pmod{10^5}$. Since $N > 10^5$, the last five digits of $N$ are $09376$, so its ten-thousands digit is $0$.

In every case, the decimal representation of $N$ contains the digit $0$, so $a(2500) = 0$.

theorem conjecture : ∃ n : ℕ, a n = 0

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

`OeisA103662.conjecture.variants.a_40`

Open: stated without proof.

$a(40)$, if it exists, is not known.

This claim is rooted in the finiteness conjecture. The most direct mathematical expression of the open problem concerning $a(40)$ is the negation of the existence of a valid base.

theorem conjecture.variants.a_40 :
  ¬ ∃ (b : ℕ), IsValidZerolessPower 40 b

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

Sources

LeanOeisA103662.conjecture · OeisA103662.conjecture.variants.a_40

Theorem$a(n) = [x^{2n}] \left(\frac{1 + x}{1 - x}\right)^n$#

The sequence is given by the combinatorial identity: $a(n) = \sum_{k = 0}^n \binom{n}{k} \binom{2n+k-1}{n-1}$ with $a(0) = 1$.

References: - A103885

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

`OeisA103885.conjecture`

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-lite-200usd-sol-nk5wh4g0vh3546nm/oeis_a103885_conjecture_0/Submission/Spec.lean#L2587.

The recurrence given below can be rewritten in the form

\[(2n+1)(2n+2)P(2,n)a(n+1) - (2n-1)(2n-2)P(2,-n)a(n-1) = Q(2,n^2)a(n),\]

where the polynomial $Q(2,n) = 4(55n^2 - 34n + 3)$ and the polynomial $P(2,n) = 5n^2 - 5n + 1$ satisfies the symmetry condition $P(2,n) = P(2,1-n)$ and has real zeros. More generally, for fixed $m = 1,2,3, \ldots$, we conjecture that the sequence $b(n) := a(mn)$ satisfies a recurrence of the form

\[( \prod_{k = 1}^{2m} (2mn + k) )P(2m,n)b(n+1) + (-1)^m( \prod_{k = 1}^{2*m} (2mn - k) ) P(2m,-n)b(n-1) = Q(2m,n^2)b(n),\]

where the polynomials $P(2m,n)$ and $Q(2m,n)$ have degree $2m$. Conjecturally, the polynomial $P(2m,n) = P(2m,1-n)$ and has real zeros in the interval [0, 1]. The $4m$ zeros of the polynomial $Q(2m,n^2)$ seem to belong to the interval $[-1, 1]$ and $4m - 2$ of these zeros appear to be approximated by the rational numbers $\pm k/(3m)$, where $1 \le k \le 3m - 2$, $k$ not a multiple of $3$.

theorem conjecture (m : ℕ) (hm : 1 ≤ m) :
    ∃ (P Q : Polynomial ℝ),
      -- P and Q have degree 2m
      P.degree = (2 * m : ℕ) ∧ Q.degree = (2 * m : ℕ) ∧
      -- The recurrence relation holds for all n >= 1
      (∀ (n : ℕ) (hn : 1 ≤ n),
        (prodFactorPlus m n * P.eval (n : ℝ)) * (aSubsequenceReal m (n + 1)) +

        ((-1 : ℝ) ^ m * prodFactorMinus m n * P.eval (-(n : ℝ))) * (aSubsequenceReal m (n - 1)) =

        (Q.eval ((n : ℝ)^2)) * (aSubsequenceReal m n)) ∧

      -- P symmetry: P(x) = P(1-x)
      (∀ x : ℝ, P.eval x = P.eval (1 - x)) ∧

      -- P has real zeros in [0, 1]: all complex zeros are real and in [0, 1]
      (∀ z : ℂ, (P.map (algebraMap ℝ ℂ)).eval z = 0 → z.im = 0 ∧ z.re ∈ (Set.Icc 0 1)) ∧

      -- Q zero properties: The zeros of Q(x^2) are real and in [-1, 1].
      (∀ z : ℂ, (Q.map (algebraMap ℝ ℂ)).eval (z^2) = 0 → z.im = 0 ∧ z.re ∈ (Set.Icc (-1) 1))

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

Sources

LeanOeisA103885.conjecture

TheoremNumber of zeros in ternary representation of $2^n$#

References: - A104320

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

`OeisA104320.conjecture`

Open: stated without proof.

Conjecture from N. J. A. Sloane: $a(n) > 0$ for $n > 15$.

theorem conjecture : ∀ n : ℕ, 15 < n → a n > 0

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

Sources

LeanOeisA104320.conjecture

TheoremArray 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

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

`OeisA105020.conjecture`

Open: stated without proof.

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

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

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

Sources

LeanOeisA105020.conjecture

TheoremConjectures associated with A105210 #

$a(1) = 393$; for $n > 1$, $a(n) = a(n-1)$ + 1 + sum of distinct prime factors of $a(n-1)$ that are $< a(n-1)$.

References: - A105210

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

`OeisA105210.conjecture_disjoint_starting_values`

Open: stated without proof.

Cormier and Selfridge found 5 starting values for which the sequences appear to not merge. The sequences were checked up to 10^8.

theorem conjecture_disjoint_starting_values :
    ∀ j k : ℕ,
      j ∈ ({1, 393, 412, 668, 932} : Set ℕ) →
      k ∈ ({1, 393, 412, 668, 932} : Set ℕ) →
      j ≠ k →
      sequenceSet j ∩ sequenceSet k = ∅

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

`OeisA105210.conjecture`

Open: stated without proof.

This suggests that there may be infinitely many different (non-merging) sequences obtained by choosing different starting values.

theorem conjecture :
  ∃ K : Set ℕ,
    Set.Infinite K ∧
    (∀ k ∈ K, 1 ≤ k) ∧
    (∀ j k : ℕ,
      j ∈ K → k ∈ K → j ≠ k →
      sequenceSet j ∩ sequenceSet k = ∅)

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

Sources

LeanOeisA105210.conjecture_disjoint_starting_values · OeisA105210.conjecture

TheoremIndicator sequence for 5 Fibonacci numbers with n digits #

$a(n) = 1$ if exactly 5 Fibonacci numbers exist with exactly $n$ digits, otherwise $0$. For the partial sums $S(n) = \sum_{k=1}^n a(k)$, it is conjectured that $\beta-2 < S(n)-\alpha n < \beta-1$, where $\alpha = \log(10)/\log(\phi) - 4$ and $\beta = \log(5)/(2\log(\phi)) - 1$.

References: - A105565

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

`OeisA105565.conjecture`

Solved: stated here; a Lean proof is at https://github.com/HaigAd/formal-conjectures/blob/327b99914ce787ab41c67ba645626982e15b0124/FormalConjectures/OEIS/105565.lean#L595.

Conjecture: $\beta-2 < S(n)-\alpha n < \beta-1$. The constants $\alpha$ and $\beta$ are as defined in the formula section.

Solved by OpenAI Codex, prompted by Adam Haig. A complete Lean 4 proof is linked by the formal_proof attribute below.

theorem conjecture (n : ℕ) (hn : 1 ≤ n) :
    betaConst - 2 < s n - alphaConst * (n : Real) ∧
      s n - alphaConst * (n : Real) < betaConst - 1

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

Sources

LeanOeisA105565.conjecture

TheoremTriangular matchstick numbers in the class of prime numbers #

$a(n) = \sum_{k = n}^{2n} p_k$, where $p_k$ is the $k$-th prime.

References: - A105720

Quoted from FormalConjectures/OEIS/105720.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 and 3 API statements, counted here but not shown.

`OeisA105720.conjecture`

Open: stated without proof.

Terms are squares at only(?) three values of $n = 3, 6, 4072$: corresponding terms are 6^2, 13^2, and 15735^2.

theorem conjecture :
    ∀ n : ℕ, 0 < n → (IsSquare (a n) ↔ (n = 3 ∨ n = 6 ∨ n = 4072))

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

Sources

LeanOeisA105720.conjecture

TheoremImaginary part of $\prod_{k=0}^n (1 + k \cdot i)$, $i = \sqrt{-1}$#

References: - A105751

Quoted from FormalConjectures/OEIS/105751.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: 1 open, 1 solved and 1 textbook result. It also has 5 test statements, counted here but not shown.

`OeisA105751.prime_divides_some_term`

Textbook result, stated without proof.

Numerical calculation suggests that a similar division holds in this case. Type 1: primes p that do not divide any element of the sequence {$a(n)$}. In this case, unlike in A105750, the set of type 1 primes is empty; that is, every prime p divides some term of this sequence.

Note: The triangular number n*(n+1)/2 divides $a(n)$ (see A164652). In particular, if $p$ is an odd prime then $p$ divides $a(p)$. For $p=2$, $2$ divides $a(4)=-40$.

theorem prime_divides_some_term (p : ℕ) (hp : p.Prime) :
    ∃ n : ℕ, a n ≠ 0 ∧ (p : ℤ) ∣ a n

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/105751.lean, line 72.

`OeisA105751.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a105751-two-adic/blob/a9692d90078c4dff1478acaaa70be2fba06a3ef9/lean/OeisA105751TwoAdicFC.lean#L980-L985.

Moll's conjecture 5.5 extends to this sequence and takes the form: (i) the $2$-adic valuation $\nu_2(a(n)) \sim n/4$ as n -> oo.

theorem conjecture :
    Tendsto (fun n ↦ (4 : ℚ) * (padicValInt 2 (a n) : ℚ) / (n : ℚ)) atTop (nhds 1)

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

`OeisA105751.conjecture.variants.moll_p_mod_4_eq_1`

Open: stated without proof.

Moll's conjecture 5.5 extends to this sequence and takes the form: (ii) for the other primes of type $2$, the p-adic valuation $\nu_p(a(n)) \sim n/(p - 1)$ as $n \rightarrow \infty$.

(Type 2 primes consists of primes p == 1 (mod 4))

theorem conjecture.variants.moll_p_mod_4_eq_1 {p : ℕ} (hp : p.Prime) (h_mod : p % 4 = 1) :
    Tendsto (fun n ↦ ((p - 1 : ℚ) * (padicValInt p (a n) : ℚ)) / (n : ℚ)) atTop (nhds 1)

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

Sources

LeanOeisA105751.prime_divides_some_term · OeisA105751.conjecture · OeisA105751.conjecture.variants.moll_p_mod_4_eq_1

TheoremFibonacci-Collatz sequence #

Fibonacci-Collatz sequence: $a(1)=1, a(2)=2$; for $n > 2$, let $\mathrm{fib} = a(n-1) + a(n-2)$; if $\mathrm{fib}$ is odd then $a(n) = 3 \cdot \mathrm{fib} + 1$ else $a(n) = \mathrm{fib}/2$.

References: - A105801

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

`OeisA105801.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a105801-lean/blob/68642a80db062bee7061437b60d31c3e7d626595/lean/OeisA105801FC.lean#L323-L351.

Conjecture: for every $k > 0$ there is an index $m$ such that all the $a(n)$ with $n > m$ have the same residue $\bmod 3^k$.

theorem conjecture :
    ∀ k : ℕ, 0 < k → ∃ m : ℕ, ∀ n : ℕ, m < n → a n ≡ a (m + 1) [MOD (3^k)]

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

Sources

LeanOeisA105801.conjecture

TheoremSum of squares of nonacci numbers #

Sum of squares of nonacci numbers (Fibonacci 9-step numbers).

References: - A107247

Quoted from FormalConjectures/OEIS/107247.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 textbook result. It also has 5 test statements, counted here but not shown.

`OeisA107247.known_prime_and_semiprimes`

Textbook result, stated without proof.

Primes in this sequence include: $a(8) = 2$. Semiprimes in this sequence include: $a(9) = 6 = 2 * 3$, $a(10) = 22 = 2 * 11$, $a(11) = 86 = 2 * 43$, $a(13) = 1366 = 2 * 683$, $a(14) = 5462 = 2 * 2731$, $a(16) = 87382 = 2 * 43691$, $a(17) = 348503 = 37 * 9419$, $a(27) = 358201316657 = 71 * 5045088967$. (Note: The OEIS comment uses 1-based indexing, so their indices are shifted by +1 compared to this formalization).

theorem known_prime_and_semiprimes :
  (a 8).Prime ∧
  (a 9).IsSemiprime ∧
  (a 10).IsSemiprime ∧
  (a 11).IsSemiprime ∧
  (a 13).IsSemiprime ∧
  (a 14).IsSemiprime ∧
  (a 16).IsSemiprime ∧
  (a 17).IsSemiprime ∧
  (a 27).IsSemiprime

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/107247.lean, line 78.

`OeisA107247.conjecture`

Open: stated without proof.

Primes in this sequence include: $a(8) = 2$, which is next?

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

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

Sources

LeanOeisA107247.known_prime_and_semiprimes · OeisA107247.conjecture

Theorem$a(n) = \sum_{i=0}^n \binom{2n-i}{n+i}$#

Alternatively the sequence a can be defined as $a(n) = \sum_{k=0}^n \binom{n+k-1}{k} F(n-k+1)$, where $F(m)$ is the $m$-th Fibonacci number. We formalize a conjecture about the number of words of length $n$ in a set $X$ being related to this sequence.

References: - A108081

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

`OeisA108081.count_words_in_x_is_a_shifted`

Solved: stated here; a Lean proof is at https://github.com/niketp03/atlas-fc-verified/blob/15e4b3a7584e218cec531aeaf71cce72a8a9ecb1/AtlasFCSolutions/OeisA108081.lean#L3720.

"The number of words of length $n$ for $n \le 12$ is given by $a(n+1)$. Is this always true?"

Formalized as $|X_n| = a(n-1)$ for $n \ge 1$, because the sequence values $a(0)=1, a(1)=2, a(2)=7$ match the examples given for word lengths $n=1, 2, 3$ respectively.

Solved: a Lean 4 proof, derived from the Atlas proofs in facebookresearch/atlas-lean, is linked in formal_proof.

theorem count_words_in_x_is_a_shifted (n : ℕ) :
    n ≥ 1 → Set.ncard (xN n) = a (n - 1)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/OEIS/108081.lean, line 96.

Sources

LeanOeisA108081.count_words_in_x_is_a_shifted

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Pentanacci \(\pi\) sequence to $a(n) = \sum_{i=0}^n…

TheoremPentanacci \(\pi\) sequence#

OeisA100478.conjecture

Sources

TheoremConjectures associated with A100800#

OeisA100800.conjecture

Sources

TheoremConjectures associated with A101779#

OeisA101779.conjecture

Sources

TheoremConjectures associated with A102371#

OeisA102371.conjecture

Sources

TheoremFloor of sum of \(\{n/k\}\)#

OeisA102722.conjecture

Sources

Theorem\(a(0) = 1\), \(a(n) = a(n-1)a(n-1) + 2\)#

OeisA102847.conjecture

Sources

TheoremNumber of decompositions of \(2n+1\) into \(2p+q\), where \(p\) and \(q\) are both odd primes#

OeisA103151.conjecture

Sources

TheoremFibonacci transform satisfying \(|a(n)| = F(n+1)\)#

OeisA103311.a_abs_eq_fib

Sources

Theorem\(a(n) = 3a(n-1) + a(n-2) - 3a(n-3)\)#

OeisA103425.conjecture

OeisA103425.conjecture.variants.nonconstant

OeisA103425.conjecture.variants.nonconstant_distinct_coeffs

Sources

TheoremSmallest power with base>1 and exponent \(n\) without digit 0#

OeisA103662.conjecture

OeisA103662.conjecture.variants.a_40

Sources

Theorem\(a(n) = [x^{2n}] \left(\frac{1 + x}{1 - x}\right)^n\)#

OeisA103885.conjecture

Sources

TheoremNumber of zeros in ternary representation of \(2^n\)#

OeisA104320.conjecture

Sources

TheoremArray read by upward antidiagonals#

OeisA105020.conjecture

Sources

TheoremConjectures associated with A105210#

OeisA105210.conjecture_disjoint_starting_values

OeisA105210.conjecture

Sources

TheoremIndicator sequence for 5 Fibonacci numbers with n digits#

OeisA105565.conjecture

Sources

TheoremTriangular matchstick numbers in the class of prime numbers#

OeisA105720.conjecture

Sources

TheoremImaginary part of \(\prod_{k=0}^n (1 + k \cdot i)\), \(i = \sqrt{-1}\)#

OeisA105751.prime_divides_some_term

OeisA105751.conjecture

OeisA105751.conjecture.variants.moll_p_mod_4_eq_1

Sources

TheoremFibonacci-Collatz sequence#

OeisA105801.conjecture

Sources

TheoremSum of squares of nonacci numbers#

OeisA107247.known_prime_and_semiprimes

OeisA107247.conjecture

Sources

Theorem\(a(n) = \sum_{i=0}^n \binom{2n-i}{n+i}\)#

OeisA108081.count_words_in_x_is_a_shifted

Sources

TheoremPentanacci \(\pi\) sequence #

`OeisA100478.conjecture`

TheoremConjectures associated with A100800 #

`OeisA100800.conjecture`

TheoremConjectures associated with A101779 #

`OeisA101779.conjecture`

TheoremConjectures associated with A102371 #

`OeisA102371.conjecture`

`OeisA102722.conjecture`

`OeisA102847.conjecture`

TheoremNumber of decompositions of \(2n+1\) into \(2p+q\), where \(p\) and \(q\) are both odd primes #

`OeisA103151.conjecture`

`OeisA103311.a_abs_eq_fib`

`OeisA103425.conjecture`

`OeisA103425.conjecture.variants.nonconstant`

`OeisA103425.conjecture.variants.nonconstant_distinct_coeffs`

TheoremSmallest power with base>1 and exponent \(n\) without digit 0 #

`OeisA103662.conjecture`

`OeisA103662.conjecture.variants.a_40`

`OeisA103885.conjecture`

`OeisA104320.conjecture`

TheoremArray read by upward antidiagonals #

`OeisA105020.conjecture`

TheoremConjectures associated with A105210 #

`OeisA105210.conjecture_disjoint_starting_values`

`OeisA105210.conjecture`

TheoremIndicator sequence for 5 Fibonacci numbers with n digits #

`OeisA105565.conjecture`

TheoremTriangular matchstick numbers in the class of prime numbers #

`OeisA105720.conjecture`

`OeisA105751.prime_divides_some_term`

`OeisA105751.conjecture`

`OeisA105751.conjecture.variants.moll_p_mod_4_eq_1`

TheoremFibonacci-Collatz sequence #

`OeisA105801.conjecture`

TheoremSum of squares of nonacci numbers #

`OeisA107247.known_prime_and_semiprimes`

`OeisA107247.conjecture`

`OeisA108081.count_words_in_x_is_a_shifted`