Least $m$ such that $m + n$… to Representations of $n$ as $x^2…

TheoremLeast $m$ such that $m + n$ divides $\mathrm{prime}(m) + \mathrm{prime}(n)$#

The sequence $a(n)$ is the least positive integer $m$ such that $m + n$ divides $\mathrm{prime}(m) + \mathrm{prime}(n)$, where $\mathrm{prime}(k)$ denotes the $k$-th prime number (with $\mathrm{prime}(1) = 2$).

References: - A247824

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

`OeisA247824.conjecture_1`

Open: stated without proof.

Conjecture: $a(n)$ exists for any $n > 0$. The existence of $a(n)$ for $n > 0$ is formalized by requiring that the defining set is nonempty (equivalently, $0 < a(n)$). - Zhi-Wei Sun, Sep 25 2014

theorem conjecture_1 (n : ℕ) (hn : 0 < n) :
    ({ m : ℕ | 0 < m ∧
      (m + n) ∣ (Nat.nth Nat.Prime (m - 1) + Nat.nth Nat.Prime (n - 1)) }).Nonempty

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

`OeisA247824.conjecture_2`

Solved: stated here without proof.

Conjecture: $a(n) < n(n-1)$ for all $n > 2$. - Zhi-Wei Sun, Sep 25 2014

Disproved by Khai-Hoan Nguyen-Dang (Oct 30 2026), who found the counterexample $n = 1322164$, for which $a(1322164) = 2636932401176 > 1748116320732 = 1322164 \cdot 1322163$.

theorem conjecture_2 : ¬ ∀ n : ℕ, 2 < n → a n < n * (n - 1)

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

Sources

LeanOeisA247824.conjecture_1 · OeisA247824.conjecture_2

TheoremLeast $m > 0$ coprime to $n$ such that $mn \mid C(m+n)$#

The sequence $a(n)$ is the least positive integer $m$ such that $\gcd(m, n) = 1$ and $m \cdot n \mid C(m+n)$, where $C(k) = \frac{1}{k+1} \binom{2k}{k}$ is the $k$-th Catalan number.

References: - A248123

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

`OeisA248123.conjecture`

Open: stated without proof.

Conjecture: $a(n)$ exists for all $n > 0$. Since $a(n)$ is defined as the infimum of a set of positive integers, existence is equivalent to $0 < a(n)$.

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

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

Sources

LeanOeisA248123.conjecture

TheoremSmallest prime factors of $2^{2^n+2} + 3$#

Smallest prime factor of $2^{2^n+2} + 3$.

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

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

`OeisA248802.a_ten_mul_add_two_eq`

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

Conjecture 1: $a(10n+2) = 67$ for $n \ge 0$. - Chai Wah Wu, Oct 21 2019

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

theorem a_ten_mul_add_two_eq (n : ℕ) : a (10 * n + 2) = 67

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

`OeisA248802.a_fifty_eight_mul_add_twenty_six_eq`

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

Conjecture 4: $a(58n+26) = 1399$ for $n \ge 0$ and when it is not covered by Conjectures 1-3. - Chai Wah Wu, Oct 21 2019

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

theorem a_fifty_eight_mul_add_twenty_six_eq (n : ℕ) :
    (¬CoveredByC1 (58 * n + 26) ∧ ¬CoveredByC2 (58 * n + 26) ∧
    ¬CoveredByC3 (58 * n + 26)) → a (58 * n + 26) = 1399

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

Sources

LeanOeisA248802.a_ten_mul_add_two_eq · OeisA248802.a_fifty_eight_mul_add_twenty_six_eq

TheoremSmallest $m \in [1, n]$ such that $\binom{n}{m}$ is evil #

The sequence $a(n)$ is the smallest $m$ with $1 \le m \le n$ such that $\binom{n}{m}$ is an evil number (A001969, having an even number of $1$s in its binary expansion), or $0$ if no such $m$ exists.

References: - A249609

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

`OeisA249609.conjecture`

Open: stated without proof.

Conjecture: there are only five $n$ ($0, 1, 2, 7, 8$) for which all entries of the $n$-th Pascal row (A007318) are odious (A000069), which is equivalent to $a(n) = 0$.

theorem conjecture (n : ℕ) :
    a n = 0 ↔ n ∈ ({0, 1, 2, 7, 8} : Finset ℕ)

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

Sources

LeanOeisA249609.conjecture

TheoremOdd part of the digital sum of $3^n$ divided by the maximal power of $3$#

The sequence $a(n)$ is the odd part of the base-$10$ digital sum of $3^n$ divided by the maximal possible power of $3$.

References: - A250131

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

`OeisA250131.conjecture_1`

Open: stated without proof.

Conjecture: Consider the sequence $b(n)$ such that $b(1)=2$, $b(2)=3$, and for $n \ge 3$, $b(n)=a(n-2)$. If we apply the Eratosthenes-like sieve to $b(n)$ and remove $1$s, then we obtain a sequence of primes. - Vladimir Shevelev, Dec 12 2014

theorem conjecture_1 : ∀ n ∈ sievedIndices, (b n).Prime

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

`OeisA250131.conjecture_2`

Open: stated without proof.

Stronger variant: the sieved sequence $b(n)$ yields the set of all primes (in some perturbed order).

Note: This stronger statement is not explicitly written on the A250131 OEIS page (which only states conjecture_1 and notes via Peter J. C. Moses that "these primes follow with some perturbation of order"), but is implied by prepending $b(1)=2, b(2)=3$ (which otherwise have no effect on the sieve since $\gcd(a(n), 6) = 1$) and by Vladimir Shevelev's analogous conjecture in the cross-referenced entries A221858 and A225039.

theorem conjecture_2 : b '' sievedIndices = {p : ℕ | p.Prime}

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

Sources

LeanOeisA250131.conjecture_1 · OeisA250131.conjecture_2

TheoremFloor of $n^2$ divided by the sum of products of consecutive divisors of $n$#

Let $n \ge 2$ be a positive integer with divisors $1 = d_1 < d_2 < \dots < d_k = n$, and let $s = d_1 d_2 + d_2 d_3 + \dots + d_{k-1} d_k$. The sequence $a(n)$ lists the values $\lfloor n^2 / s \rfloor$.

References: - A251758

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

`OeisA251758.conjecture`

Open: stated without proof.

Let $p\#_i$ denote the $i$-th primorial (Nat.kthPrimorial i). For $n = 8$, the primorial ratios $x = p\#_{12}/p\#_4, p\#_{13}/p\#_4, p\#_{14}/p\#_4, p\#_{15}/p\#_4, p\#_{16}/p\#_4, \dots$ satisfy $a(x) = 8$. Is $p\#_{12}/p\#_4 = 35336848261$ the least $x \ge 2$ such that $a(x) = 8$?

"For $n=8$, $x = p\#12/p\#4, p\#13/p\#4, p\#14/p\#4, p\#15/p\#4, p\#16/p\#4$, etc. But is $p\#12/p\#4$ the least such $x$?" - Robert G. Wilson v, Dec 18 2014

theorem conjecture :
    IsLeast {x : ℕ | 2 ≤ x ∧ a x = 8}
      (Nat.kthPrimorial 12 / Nat.kthPrimorial (Nat.primeCounting' 8))

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

Sources

LeanOeisA251758.conjecture

TheoremRepresentations of $n$ as the sum of two pentagonal and a generalized decagonal number #

The sequence $a(n)$ counts the number of ordered ways to write $n$ as the sum of a pentagonal number $\frac{x(3x-1)}{2}$ ($x \ge 0$), a second pentagonal number $\frac{y(3y+1)}{2}$ ($y \ge 0$), and a generalized decagonal number $m(4m-3)$ ($m \in \mathbb{Z}$).

References: - A253187

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

`OeisA253187.conjecture_1`

Open: stated without proof.

Conjecture: $a(n) > 0$ for all $n$. - Zhi-Wei Sun

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

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

`OeisA253187.conjecture_2`

Open: stated without proof.

Conjecture: For any ordered pair $(k, m)$ among $(5,7), (5,9), (5,13), (6,5), (6,7), (7,5)$, each nonnegative integer $n$ can be written as the sum of a $k$-gonal number, a second $k$-gonal number, and a generalized $m$-gonal number. - Zhi-Wei Sun

theorem conjecture_2 (k m : ℕ) (hkm : (k, m) ∈ cPairs) (n : ℕ) :
    ∃ x y : ℕ, ∃ z : ℤ,
      Nat.polygonalNumber k x + Nat.generalizedPolygonalNumber k (-(y : ℤ)) +
        Nat.generalizedPolygonalNumber m z = n

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

Sources

LeanOeisA253187.conjecture_1 · OeisA253187.conjecture_2

TheoremRepresentations of $n$ as a sum of generalized heptagonal, octagonal, and nonagonal numbers #

The sequence $a(n)$ counts the number of ways to write $n$ as the sum of a generalized heptagonal number $G_7(k) = \frac{5k^2 - 3k}{2}$ ($k \in \mathbb{Z}$), an octagonal number $P_8(x) = x(3x - 2)$ ($x \ge 0$), and a nonagonal number $P_9(y) = \frac{y(7y - 5)}{2}$ ($y \ge 0$).

References: - A255916

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

`OeisA255916.conjecture_1`

Open: stated without proof.

Conjecture: $a(n) > 0$ for all $n$. - Zhi-Wei Sun

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

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

`OeisA255916.conjecture_2`

Open: stated without proof.

Conjecture (i): For $k \ge j \ge 3$, every nonnegative integer can be written as the sum of a generalized heptagonal number, a $j$-gonal number and a $k$-gonal number, if and only if $(j, k)$ is among the following ordered pairs: $(3, k)$ ($k = 3..19, 21..24, 26, 27, 29, 30$), $(4, k)$ ($k = 4..11, 13, 14, 17, 19, 20, 23, 26$), $(5, 6), (5, 9), (6, 7), (8, 9)$. - Zhi-Wei Sun

theorem conjecture_2 (j k : ℕ) (hjk : 3 ≤ j ∧ j ≤ k) :
    (∀ n : ℕ, IsSumOfGmPjPk 7 n j k) ↔ (j, k) ∈ sunPolygonalPairsSet1

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

`OeisA255916.conjecture_3`

Open: stated without proof.

Conjecture (ii): For $k \ge j \ge 3$, every nonnegative integer can be written as the sum of a generalized pentagonal number, a $j$-gonal number and a $k$-gonal number, if and only if $(j, k)$ is among the following ordered pairs: $(3, k)$ ($k = 3..20, 22, 24, 25, 28..30, 32, 37$), $(4, k)$ ($k = 4..13, 15, 16, 18, 20..25, 27, 28, 31, 33, 34$), $(5, k)$ ($k = 6..12, 20$), $(6, k)$ ($k = 7..10$), $(7, 9), (7, 11), (8, 10), (9, 11)$. - Zhi-Wei Sun

theorem conjecture_3 (j k : ℕ) (hjk : 3 ≤ j ∧ j ≤ k) :
    (∀ n : ℕ, IsSumOfGmPjPk 5 n j k) ↔ (j, k) ∈ sunPolygonalPairsSet2

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

Sources

LeanOeisA255916.conjecture_1 · OeisA255916.conjecture_2 · OeisA255916.conjecture_3

TheoremPartitions of $n$ into distinct non-squarefree parts for $n > 23$#

a: Number of partitions of $n$ into distinct parts that are not squarefree. This is the number of finite subsets of positive integers $P$ such that $\sum_{k \in P} k = n$ and every element $k \in P$ is not squarefree.

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

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

`OeisA256012.a_pos_of_gt`

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

Conjecture: $a(n) > 0$ for $n > 23$.

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

theorem a_pos_of_gt (n : ℕ) (hn : n > 23) : a n > 0

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

Sources

LeanOeisA256012.a_pos_of_gt

TheoremWays to write $n$ as the sum of three elements of $\{\lfloor T(x)/3 \rfloor : x \ge 1\}$#

The sequence $a(n)$ counts the number of ways to write $n$ as the sum of three unordered elements of the set $\{\lfloor T(x)/3 \rfloor : x = 1, 2, 3, \dots\}$, where $T(x) = \frac{x(x+1)}{2}$ is the $x$-th triangular number.

References: - A256544

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

`OeisA256544.conjecture`

Open: stated without proof.

Conjecture: For any positive integer $m$, every nonnegative integer $n$ can be written as $\lfloor T(x)/m \rfloor + \lfloor T(y)/m \rfloor + \lfloor T(z)/m \rfloor$ with $x, y, z$ nonnegative integers.

theorem conjecture (m : ℕ) (hm : 0 < m) (n : ℕ) :
    ∃ x y z : ℕ, n = Nat.triangular x / m + Nat.triangular y / m + Nat.triangular z / m

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

Sources

LeanOeisA256544.conjecture

TheoremAsymptotics of an inner sum formula for $a(n)$#

The inner sum of the formula used in a:

\[\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}\]

a: A total of $n$ married couples, including a mathematician M and his wife, are to be seated at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies are seated at every other chair, M is the first man allowed to choose one of the remaining chairs. The sequence gives the number of ways of seating the other men, with no man seated next to his wife, if M chooses the chair that is 9 seats clockwise from his wife's chair.

\[a(n) = \begin{cases} 0 & \text{if } n \le 5 \cr \sum_{k=0}^{n-1}(-1)^k(n-k-1)! \sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j} & \text{if } n > 5 \end{cases}\]

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

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

`OeisA258667.a_is_equivalent_asymptoticTerm`

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

Conjecture: $a(n) \sim e^{-2} \cdot n! / (n-2)$.

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

theorem a_is_equivalent_asymptoticTerm :
    IsEquivalent atTop (fun n : ℕ => (a n : ℝ)) asymptoticTerm

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

Sources

LeanOeisA258667.a_is_equivalent_asymptoticTerm

TheoremCatalan numbers modulo $6$#

The sequence $a(n) = C_n \bmod 6$, where $C_n = \frac{1}{n+1} \binom{2n}{n}$ is the $n$-th Catalan number (A000108).

References: - A259667

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

`OeisA259667.conjecture_1`

Open: stated without proof.

It is conjectured that the only $k$ which yield $a(2^k - 1) = 1$ are $k = 0, 1$ and $5$.

theorem conjecture_1 (k : ℕ) :
    a (2 ^ k - 1) = 1 ↔ k = 0 ∨ k = 1 ∨ k = 5

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

`OeisA259667.conjecture_2`

Open: stated without proof.

Conjecture: The only $k$ which yield $a(2^k - 1) = 5$ are $k = 2, 8$.

theorem conjecture_2 (k : ℕ) :
    a (2 ^ k - 1) = 5 ↔ k = 2 ∨ k = 8

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

Sources

LeanOeisA259667.conjecture_1 · OeisA259667.conjecture_2

TheoremA GCD-Driven Sequence with Universal Jumps #

OEIS A260194 begins with three ones and then adds the greatest common divisor of the current term and the term two places earlier. The open question asks whether every positive integer occurs as an adjacent difference.

References: - OEIS A260194

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

`OeisA260194.conjecture`

Open: stated without proof.

Does every positive integer occur as a difference in this sequence?

theorem conjecture :
    ∀ d > 0, ∃ n, a (n + 1) = a n + d

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

Sources

LeanOeisA260194.conjecture

TheoremPrime values in recurrence $a(n+1) = |a(n) - \gcd(a(n), 7n+6)|$#

The sequence is defined by $a(1) = 1$ and $a(n+1) = |a(n) - \gcd(a(n), 7n+6)|$ for $n \ge 1$.

References: - A261307

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

`OeisA261307.conjecture`

Open: stated without proof.

It is conjectured that for all $n > 2$, $a(n) = 0$ implies that $7n+6 = a(n+1)$ is prime, cf. A186259.

theorem conjecture (n : ℕ) (hn : 2 < n) (ha : a n = 0) : Nat.Prime (7 * n + 6)

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

Sources

LeanOeisA261307.conjecture

TheoremPrimes $p$ such that $n - (p n' - 1)$ and $n + (p n' - 1)$ are both prime #

Number of primes $p$ such that $n - (p n' - 1)$ and $n + (p n' - 1)$ are both prime, where $n'$ is $1$ or $2$ according as $n$ is odd or even.

References: - A261627 - Conjectures involving primes and quadratic forms by Zhi-Wei Sun, arXiv:1211.1588 (2012-2015)

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

`OeisA261627.conjecture_1`

Open: stated without proof.

Conjecture: $a(n) > 0$ for all $n > 6$.

theorem conjecture_1 (n : ℕ) (hn : 6 < n) : 0 < a n

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

`OeisA261627.conjecture_2`

Open: stated without proof.

Conjecture: $a(n) = 1$ only for $n = 5, 7, 10, 11, 12, 19, 22, 30, 34, 44, 46, 72, 142$.

theorem conjecture_2 (n : ℕ) :
    a n = 1 ↔ n ∈ singletons

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

Sources

LeanOeisA261627.conjecture_1 · OeisA261627.conjecture_2

TheoremSums of four binary palindromes #

Number of ordered quadruples $(u, v, w, x)$ of binary palindromes (see A006995) with $u + v + w + x = n$.

References: - A261680 - Sums of Palindromes: an Approach via Nested-Word Automata by Aayush Rajasekaran, Jeffrey Shallit, and Tim Smith, arXiv:1706.10206 (2017)

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

`OeisA261680.conjecture`

Solved: stated here without proof.

Every number is the sum of four binary palindromes, i.e., $a(n) > 0$ for all $n$. Originally stated as a conjecture on OEIS; proved by Rajasekaran, Shallit, and Smith (2017).

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

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

Sources

LeanOeisA261680.conjecture

TheoremRefining Lagrange's four-square theorem with $(5x^2 + 7y^2 + 9z^2)yz$ a square #

Number of ordered ways to write $n$ as $x^2 + y^2 + z^2 + w^2$ with $(5x^2 + 7y^2 + 9z^2)yz$ a square, where $x, y, z, w$ are nonnegative integers with $z > 0$.

References: - A261876 - Refining Lagrange's four-square theorem by Zhi-Wei Sun, arXiv:1604.06723 (2016) - arXiv:2608.11941

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

`OeisA261876.conjecture_1`

Open: stated without proof.

Conjecture (i): $a(n) > 0$ for all $n > 0$.

theorem conjecture_1 (n : ℕ) (hn : 0 < n) : 0 < a n

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

`OeisA261876.conjecture_2`

Solved: stated here without proof.

Conjecture (i): $a(n) = 1$ only for $n = 4^k m$ ($k = 0, 1, 2, \dots$ and $m \in \{1, 7, 23, 647, 863\}$).

Disproved in arXiv:2608.11941 at $n = 69383$, where $(x, y, z, w) = (187, 147, 6, 113)$ is the unique representation, so $a(69383) = 1$.

theorem conjecture_2 :
    ¬ ∀ n : ℕ, (a n = 1 ↔ ∃ k : ℕ, ∃ m ∈ specialSet, n = 4 ^ k * m)

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

`OeisA261876.conjecture_3`

Open: stated without proof.

Conjecture (ii): For each triple $(c_1, c_2, c_3) \in \{(1,8,20), (3,5,15), (6,14,4), (7,29,5), (18,38,18), (39,81,51), (42,98,14)\}$, any natural number can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers such that $xy(c_1 x^2 + c_2 y^2 + c_3 z^2)$ is a square.

theorem conjecture_3 (t : ℕ × ℕ × ℕ) (ht : t ∈ triples) (n : ℕ) :
    ∃ x y z w : ℕ, n = x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2 ∧
      IsSquare (x * y * (t.1 * x ^ 2 + t.2.1 * y ^ 2 + t.2.2 * z ^ 2))

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

Sources

LeanOeisA261876.conjecture_1 · OeisA261876.conjecture_2 · OeisA261876.conjecture_3

TheoremAdditive decompositions of $\pi(T(n))$#

Number of ways to write $\pi(T(n)) = \pi(T(k)) + \pi(T(m))$ with $1 < k < m < n$, where $T(x) = \frac{x(x+1)}{2}$ is the $x$-th triangular number and $\pi(x)$ is the number of primes not exceeding $x$.

References: - A262403 - Problems on combinatorial properties of primes by Zhi-Wei Sun, arXiv:1402.6641 (2014)

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

`OeisA262403.conjecture_1`

Open: stated without proof.

Conjecture (i): $a(n) > 0$ for all $n > 4$.

theorem conjecture_1 (n : ℕ) (hn : 4 < n) : 0 < a n

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

`OeisA262403.conjecture_2`

Open: stated without proof.

Conjecture (i): $a(n) = 1$ only for $n = 5, 6, 7, 10, 12, 32, 38, 445, 727$.

theorem conjecture_2 (n : ℕ) (hn : 4 < n) :
    a n = 1 ↔ n ∈ singletons

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

`OeisA262403.conjecture_3`

Open: stated without proof.

Conjecture (ii), first assertion: All numbers $\pi(T(n))$ ($n = 1, 2, 3, \dots$) are pairwise distinct.

theorem conjecture_3 (m n : ℕ) (hm : 0 < m) (hn : 0 < n)
    (h : primeCountTriangular m = primeCountTriangular n) : m = n

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

`OeisA262403.conjecture_4`

Open: stated without proof.

Conjecture (ii), second assertion: If $\sum_{i=j}^{k} \frac{1}{\pi(T(i))}$ and $\sum_{r=s}^{t} \frac{1}{\pi(T(r))}$ with $1 < j \le k$ and $j \le s \le t$ have the same fractional part but $(j, k) \ne (s, t)$, then $j = 2$, $k = 5$, and $s = t = 4$.

theorem conjecture_4 (j k s t : ℕ) (hj : 1 < j) (hjk : j ≤ k) (hjs : j ≤ s)
    (hst : s ≤ t) (hne : (j, k) ≠ (s, t))
    (h : Int.fract (∑ i ∈ Finset.Icc j k, (primeCountTriangular i : ℚ)⁻¹) =
         Int.fract (∑ r ∈ Finset.Icc s t, (primeCountTriangular r : ℚ)⁻¹)) :
    j = 2 ∧ k = 5 ∧ s = 4 ∧ t = 4

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

Sources

LeanOeisA262403.conjecture_1 · OeisA262403.conjecture_2 · OeisA262403.conjecture_3 · OeisA262403.conjecture_4

TheoremAdditive decompositions of $\pi(\frac{n(n+1)}{2} + 1)$#

Number of ways to write $\pi(\frac{n(n+1)}{2} + 1) = \pi(\frac{k(k+1)}{2} + 1) + \pi(\frac{m(m+1)}{2} + 1)$ with $0 < k < m < n$, where $\pi(x)$ is the prime-counting function.

References: - A262446 - Problems on combinatorial properties of primes by Zhi-Wei Sun, arXiv:1402.6641 (2014)

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

`OeisA262446.conjecture_1`

Open: stated without proof.

Conjecture: $a(n) > 0$ for all $n > 3$.

theorem conjecture_1 (n : ℕ) (hn : 3 < n) : 0 < a n

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

`OeisA262446.conjecture_2`

Open: stated without proof.

Conjecture: $a(n) = 1$ only for $n = 4, 6, 11, 21, 54, 253, 325$.

theorem conjecture_2 (n : ℕ) (hn : 3 < n) :
    a n = 1 ↔ n ∈ singletons

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

Sources

LeanOeisA262446.conjecture_1 · OeisA262446.conjecture_2

TheoremRepresentations of $n$ as $x^2 + \phi(y^2) + \phi(z^2)$#

Number of ordered ways to write $n$ as $x^2 + \phi(y^2) + \phi(z^2)$ ($x \ge 0$ and $0 < y \le z$) with $y$ or $z$ prime, where $\phi(\cdot)$ is Euler's totient function.

References: - A262781

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

`OeisA262781.conjecture_1`

Open: stated without proof.

Conjecture (i): $a(n) > 0$ for all $n > 6$.

theorem conjecture_1 (n : ℕ) (hn : 6 < n) : 0 < a n

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

`OeisA262781.conjecture_2`

Open: stated without proof.

Conjecture (i): $a(n) = 1$ only for $n = 3, 5, 9, 10, 17, 20, 24, 25, 31, 36, 45, 73, 80, 101, 136, 145, 388, 649$.

theorem conjecture_2 (n : ℕ) :
    a n = 1 ↔ n ∈ singletons

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

`OeisA262781.conjecture_3`

Open: stated without proof.

Conjecture (ii): For any integer $n > 4$, we can write $2n$ as $\phi(p^2) + \phi(x^2) + \phi(y^2)$ with $p$ prime and $p \le x \le y$.

theorem conjecture_3 (n : ℕ) (hn : 4 < n) :
    ∃ p x y : ℕ, p.Prime ∧ p ≤ x ∧ x ≤ y ∧
      2 * n = Nat.totient (p ^ 2) + Nat.totient (x ^ 2) + Nat.totient (y ^ 2)

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

Sources

LeanOeisA262781.conjecture_1 · OeisA262781.conjecture_2 · OeisA262781.conjecture_3

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Least \(m\) such that \(m + n\)… to Representations of \(n\) as $x^2…

TheoremLeast \(m\) such that \(m + n\) divides \(\mathrm{prime}(m) + \mathrm{prime}(n)\)#

OeisA247824.conjecture_1

OeisA247824.conjecture_2

Sources

TheoremLeast \(m > 0\) coprime to \(n\) such that \(mn \mid C(m+n)\)#

OeisA248123.conjecture

Sources

TheoremSmallest prime factors of \(2^{2^n+2} + 3\)#

OeisA248802.a_ten_mul_add_two_eq

OeisA248802.a_fifty_eight_mul_add_twenty_six_eq

Sources

TheoremSmallest \(m \in [1, n]\) such that \(\binom{n}{m}\) is evil#

OeisA249609.conjecture

Sources

TheoremOdd part of the digital sum of \(3^n\) divided by the maximal power of \(3\)#

OeisA250131.conjecture_1

OeisA250131.conjecture_2

Sources

TheoremFloor of \(n^2\) divided by the sum of products of consecutive divisors of \(n\)#

OeisA251758.conjecture

Sources

TheoremRepresentations of \(n\) as the sum of two pentagonal and a generalized decagonal number#

OeisA253187.conjecture_1

OeisA253187.conjecture_2

Sources

TheoremRepresentations of \(n\) as a sum of generalized heptagonal, octagonal, and nonagonal numbers#

OeisA255916.conjecture_1

OeisA255916.conjecture_2

OeisA255916.conjecture_3

Sources

TheoremPartitions of \(n\) into distinct non-squarefree parts for \(n > 23\)#

OeisA256012.a_pos_of_gt

Sources

TheoremWays to write \(n\) as the sum of three elements of \(\{\lfloor T(x)/3 \rfloor : x \ge 1\}\)#

OeisA256544.conjecture

Sources

TheoremAsymptotics of an inner sum formula for \(a(n)\)#

OeisA258667.a_is_equivalent_asymptoticTerm

Sources

TheoremCatalan numbers modulo \(6\)#

OeisA259667.conjecture_1

OeisA259667.conjecture_2

Sources

TheoremA GCD-Driven Sequence with Universal Jumps#

OeisA260194.conjecture

Sources

TheoremPrime values in recurrence \(a(n+1) = |a(n) - \gcd(a(n), 7n+6)|\)#

OeisA261307.conjecture

Sources

TheoremPrimes \(p\) such that \(n - (p n' - 1)\) and \(n + (p n' - 1)\) are both prime#

OeisA261627.conjecture_1

OeisA261627.conjecture_2

Sources

TheoremSums of four binary palindromes#

OeisA261680.conjecture

Sources

TheoremRefining Lagrange's four-square theorem with \((5x^2 + 7y^2 + 9z^2)yz\) a square#

OeisA261876.conjecture_1

OeisA261876.conjecture_2

OeisA261876.conjecture_3

Sources

TheoremAdditive decompositions of \(\pi(T(n))\)#

OeisA262403.conjecture_1

OeisA262403.conjecture_2

OeisA262403.conjecture_3

OeisA262403.conjecture_4

Sources

TheoremAdditive decompositions of \(\pi(\frac{n(n+1)}{2} + 1)\)#

OeisA262446.conjecture_1

OeisA262446.conjecture_2

Sources

TheoremRepresentations of \(n\) as \(x^2 + \phi(y^2) + \phi(z^2)\)#

OeisA262781.conjecture_1

OeisA262781.conjecture_2

OeisA262781.conjecture_3

Sources

`OeisA247824.conjecture_1`

`OeisA247824.conjecture_2`

`OeisA248123.conjecture`

`OeisA248802.a_ten_mul_add_two_eq`

`OeisA248802.a_fifty_eight_mul_add_twenty_six_eq`

TheoremSmallest \(m \in [1, n]\) such that \(\binom{n}{m}\) is evil #

`OeisA249609.conjecture`

`OeisA250131.conjecture_1`

`OeisA250131.conjecture_2`

`OeisA251758.conjecture`

TheoremRepresentations of \(n\) as the sum of two pentagonal and a generalized decagonal number #

`OeisA253187.conjecture_1`

`OeisA253187.conjecture_2`

TheoremRepresentations of \(n\) as a sum of generalized heptagonal, octagonal, and nonagonal numbers #

`OeisA255916.conjecture_1`

`OeisA255916.conjecture_2`

`OeisA255916.conjecture_3`

`OeisA256012.a_pos_of_gt`

`OeisA256544.conjecture`

`OeisA258667.a_is_equivalent_asymptoticTerm`

`OeisA259667.conjecture_1`

`OeisA259667.conjecture_2`

TheoremA GCD-Driven Sequence with Universal Jumps #

`OeisA260194.conjecture`

`OeisA261307.conjecture`

TheoremPrimes \(p\) such that \(n - (p n' - 1)\) and \(n + (p n' - 1)\) are both prime #

`OeisA261627.conjecture_1`

`OeisA261627.conjecture_2`

TheoremSums of four binary palindromes #

`OeisA261680.conjecture`

TheoremRefining Lagrange's four-square theorem with \((5x^2 + 7y^2 + 9z^2)yz\) a square #

`OeisA261876.conjecture_1`

`OeisA261876.conjecture_2`

`OeisA261876.conjecture_3`

`OeisA262403.conjecture_1`

`OeisA262403.conjecture_2`

`OeisA262403.conjecture_3`

`OeisA262403.conjecture_4`

`OeisA262446.conjecture_1`

`OeisA262446.conjecture_2`

`OeisA262781.conjecture_1`

`OeisA262781.conjecture_2`

`OeisA262781.conjecture_3`