Triples summing to $n$ with… to Ordered ways to write $2n = p +…

TheoremTriples summing to $n$ with $2m+1$ and $2m^3+1$ prime #

Number of ways to write $n = x + y + z$ with $x \le y \le z$, where $x, y, z$ are positive integers such that $2m + 1$ and $2m^3 + 1$ are both prime for $m \in \{x, y, z\}$.

References: - A230507

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

`OeisA230507.conjecture_1`

Open: stated without proof.

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

theorem conjecture_1 (n : ℕ) (hn : n > 2) : a n > 0

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

`OeisA230507.conjecture_2`

Open: stated without proof.

Conjecture (ii): Any integer $n > 8$ can be written as $x + y + z$ ($x, y, z > 0$) with $2x + 1, 2y + 1, 2z - 1, 2x^4 - 1, 2y^4 - 1, 2z^4 - 1$ all prime.

theorem conjecture_2 (n : ℕ) (hn : n > 8) :
    ∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧ x + y + z = n ∧
      (2 * x + 1).Prime ∧ (2 * y + 1).Prime ∧ (2 * z - 1).Prime ∧
      (2 * x ^ 4 - 1).Prime ∧ (2 * y ^ 4 - 1).Prime ∧ (2 * z ^ 4 - 1).Prime

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

Sources

LeanOeisA230507.conjecture_1 · OeisA230507.conjecture_2

TheoremSmallest $n$-th power equal to a sum of consecutive immediately preceding positive $n$-th powers #

Smallest $n$-th power equal to a sum of some consecutive, immediately preceding, positive $n$-th powers, or $0$ if none.

References: - A230718

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

`OeisA230718.conjecture`

Open: stated without proof.

Is $a(n) \ne 0$ for any $n > 3$?

theorem conjecture : ∃ n > 3, a n ≠ 0

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

Sources

LeanOeisA230718.conjecture

TheoremSum of two numbers with prime conditions #

Number of ways to write $n = x+y$, for $x,y > 0$ such that $2^x + y$ is prime.

Zhi-Wei Sun has offered a $1000 prize for the first proof.

References: - A231201 - Zhi-Wei Sun, "Table of n, a(n) for n = 1..10000", "Write n = k + m with 2^k + m prime", a message to Number Theory List, Nov. 16, 2013, "On a^n+ bn modulo m", arXiv:1312.1166 [math.NT], 2013-2014, "Problems on combinatorial properties of primes", arXiv:1402.6641 [math.NT], 2014-2015.

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

`OeisA231201.conjecture`

Open: stated without proof.

The conjecture for sequence A231201: for any $n > 1$, there exist $x, y > 0$ such that $n = x + y$ and $2^x + y$ is prime.

theorem conjecture (n : ℕ) (hn : 1 < n) : A n

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

Sources

LeanOeisA231201.conjecture

TheoremWays to write $n = x + y$ with $2^x + y(y+1)/2$ prime #

Number of ways to write $n = x + y$ ($x, y > 0$) with $2^x + y(y+1)/2$ prime.

References: - A231577

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

`OeisA231577.conjecture`

Open: stated without proof.

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

theorem conjecture (n : ℕ) (hn : n > 1) : a n > 0

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

Sources

LeanOeisA231577.conjecture

TheoremSequence designed to show there are infinitely many primes congruent to $1$ modulo $4$#

The sequence defined by $a(0) = 1$, $a(1) = 5$, and for $n > 1$, $a(n) = (a(n-1) - 1) \cdot a(n-1)^2 + 1 = 1 + 4 \prod_{i=1}^{n-1} a(i)^2$.

References: - A231830

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

`OeisA231830.conjecture`

Open: stated without proof.

Similarly to Sylvester's sequence (A000058), it is unknown if all terms are squarefree.

theorem conjecture : ∀ n : ℕ, Squarefree (a n)

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

Sources

LeanOeisA231830.conjecture

TheoremRepresentations with prime conditions #

Any integer $n > 1$ can be written as $x + y$ with $x, y > 0$ such that both $x + ny$ and $x^2 + ny^2$ are prime.

Zhi-Wei Sun has offered a $200 prize for the first proof.

References: - A232174 - Z.-W. Sun, "Conjectures on representations involving primes," in: M. Nathanson (ed.), Combinatorial and Additive Number Theory II: CANT, Springer Proc. in Math. & Stat., Vol. 220, Springer, 2017, pp. 279-310. https://arxiv.org/abs/1211.1588 - D.A. Cox, "Primes of the Form x² + ny²," John Wiley & Sons, 1989.

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

`OeisA232174.conjecture`

Open: stated without proof.

Zhi-Wei Sun's Conjecture (A232174): Any integer $n > 1$ can be written as $x + y$ with $x, y > 0$ such that both $x + ny$ and $x^2 + ny^2$ are prime.

theorem conjecture (n : ℕ) (hn : 1 < n) : A n

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

Sources

LeanOeisA232174.conjecture

TheoremWays to write $n = x + y$ with $nx + y$ and $ny - x$ both prime #

Number of ways to write $n = x + y$ ($x, y > 0$) with $nx + y$ and $ny - x$ both prime.

References: - A232194

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

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

`OeisA232194.conjecture_1`

Open: stated without proof.

Conjecture (i), part 1: $a(n) > 0$ for all $n > 2$.

theorem conjecture_1 (n : ℕ) (hn : n > 2) : a n > 0

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

`OeisA232194.conjecture_2`

Open: stated without proof.

Conjecture (i), part 2: $a(n) = 1$ only for $n = 3, 4, 6, 20, 24$.

theorem conjecture_2 (n : ℕ) :
    a n = 1 ↔ n ∈ ({3, 4, 6, 20, 24} : Finset ℕ)

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

`OeisA232194.conjecture_3`

Open: stated without proof.

Conjecture (ii): Any positive integer $n$ not among $1, 30, 54$ can be written as $x + y$ ($x, y > 0$) with $nx + y$ and $ny + x$ both prime.

theorem conjecture_3 (n : ℕ) (hn : n > 0) (hne : n ∉ ({1, 30, 54} : Finset ℕ)) :
    ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
      (n * x + y).Prime ∧ (n * y + x).Prime

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

`OeisA232194.conjecture_4`

Open: stated without proof.

Conjecture (iii): Each integer $n > 1$ not equal to $8$ can be expressed as $x + y$ ($x, y > 0$) with $nx^2 + y$ prime.

theorem conjecture_4 (n : ℕ) (hn : n > 1) (hne : n ≠ 8) :
    ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧ (n * x ^ 2 + y).Prime

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

`OeisA232194.conjecture_5`

Open: stated without proof.

Conjecture (iii), variant: Each integer $n > 1$ not equal to $8$ can be expressed as $x + y$ ($x, y > 0$) with $x^4 + ny$ prime.

theorem conjecture_5 (n : ℕ) (hn : n > 1) (hne : n ≠ 8) :
    ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧ (x ^ 4 + n * y).Prime

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

`OeisA232194.conjecture_6`

Open: stated without proof.

Conjecture (iv): Any integer $n > 5$ can be written as $p + q$ ($q > 0$) with $p$ and $nq^2 + 1$ both prime.

theorem conjecture_6 (n : ℕ) (hn : n > 5) :
    ∃ p q : ℕ, 0 < q ∧ p + q = n ∧ p.Prime ∧ (n * q ^ 2 + 1).Prime

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

Sources

LeanOeisA232194.conjecture_1 · OeisA232194.conjecture_2 · OeisA232194.conjecture_3 · OeisA232194.conjecture_4 · OeisA232194.conjecture_5 · OeisA232194.conjecture_6

TheoremLeast $m > 0$ such that $\{2^k - k : k = 1, \dots, m\}$ covers all residues modulo $n$#

For $n \ge 1$, $a(n)$ is the least positive integer $m$ such that $\{2^k - k : k = 1, \dots, m\}$ contains a complete system of residues modulo $n$.

References: - A232616 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.

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

`OeisA232616.conjecture_1`

Solved: stated here without proof.

Conjecture (i): $a(n) < 2 \cdot (\text{prime}(n) - 1)$ for all $n > 0$, where $\text{prime}(n)$ is the $n$-th prime number (1-indexed).

Disproved for $n = 550172$ in the OEIS Open project, see T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941.

theorem conjecture_1 : ¬ ∀ n > 0, a n < 2 * (Nat.nth Nat.Prime (n - 1) - 1)

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

`OeisA232616.conjecture_2`

Open: stated without proof.

Conjecture (ii), first equation: The Diophantine equation $x^n - n = y^m$ with $m, n, x, y > 1$ only has two integral solutions: $2^5 - 5 = 3^3$ and $2^7 - 7 = 11^2$.

theorem conjecture_2 (x y n m : ℕ) (hx : 1 < x) (hy : 1 < y) (hn : 1 < n) (hm : 1 < m) :
    x ^ n - n = y ^ m ↔ (x = 2 ∧ n = 5 ∧ y = 3 ∧ m = 3) ∨ (x = 2 ∧ n = 7 ∧ y = 11 ∧ m = 2)

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

`OeisA232616.conjecture_3`

Open: stated without proof.

Conjecture (ii), second equation: The Diophantine equation $x^n + n = y^m$ with $m, n, x, y > 1$ only has two integral solutions: $5^2 + 2 = 3^3$ and $5^3 + 3 = 2^7$.

theorem conjecture_3 (x y n m : ℕ) (hx : 1 < x) (hy : 1 < y) (hn : 1 < n) (hm : 1 < m) :
    x ^ n + n = y ^ m ↔ (x = 5 ∧ n = 2 ∧ y = 3 ∧ m = 3) ∨ (x = 5 ∧ n = 3 ∧ y = 2 ∧ m = 7)

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

Sources

LeanOeisA232616.conjecture_1 · OeisA232616.conjecture_2 · OeisA232616.conjecture_3

TheoremRepresentations $n = k^2 + m$ ($0 < k^2 \le m$) with $\sigma(k^2) + \phi(m)$ prime #

Let $\sigma$ denote the sum-of-divisors function and $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the representations $n = k^2 + m$ ($0 < k^2 \le m$) such that $\sigma(k^2) + \phi(m)$ is prime.

References: - A233544

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

`OeisA233544.conjecture_1`

Open: stated without proof.

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

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

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

`OeisA233544.conjecture_2`

Open: stated without proof.

Conjecture (ii): Any integer $n > 1$ can be written as $k + m$ with $k > 0$ and $m > 0$ such that $\sigma(k)^2 + \phi(m)$ is prime. - Zhi-Wei Sun

theorem conjecture_2 (n : ℕ) (hn : 1 < n) :
    ∃ k m : ℕ, 0 < k ∧ 0 < m ∧ n = k + m ∧ Nat.Prime (σ 1 k ^ 2 + m.totient)

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

`OeisA233544.conjecture_3`

Open: stated without proof.

Conjecture (ii): Any integer $n > 1$ can be written as $k + m$ with $k > 0$ and $m > 0$ such that $\sigma(k) + \phi(m)^2$ is prime. - Zhi-Wei Sun

theorem conjecture_3 (n : ℕ) (hn : 1 < n) :
    ∃ k m : ℕ, 0 < k ∧ 0 < m ∧ n = k + m ∧ Nat.Prime (σ 1 k + m.totient ^ 2)

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

Sources

LeanOeisA233544.conjecture_1 · OeisA233544.conjecture_2 · OeisA233544.conjecture_3

TheoremNumber of ways to write $n = p + q$ ($q > 0$) with $p$ and $(\phi(p)\phi(q))^4 + 1$ prime #

Let $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the representations $n = p + q$ ($q > 0$) where $p$ and $(\phi(p)\phi(q))^4 + 1$ are both prime.

References: - A233549

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

`OeisA233549.conjecture_1`

Open: stated without proof.

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

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

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

`OeisA233549.conjecture_2`

Open: stated without proof.

Conjecture (ii): If $n > 2$ is not equal to $26$, then there is a prime $p < n$ with $(\phi(p)\phi(n-p))^2 + 1$ prime.

theorem conjecture_2 (n : ℕ) (hn : 2 < n) (hne : n ≠ 26) :
    ∃ p < n, p.Prime ∧ Nat.Prime ((p.totient * (n - p).totient) ^ 2 + 1)

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

`OeisA233549.conjecture_3`

Open: stated without proof.

Conjecture (iii): If $n > 3$ is different from $9$ and $16$, then there is a prime $p < n$ with $((p+1)\phi(n-p))^2 + 1$ prime.

theorem conjecture_3 (n : ℕ) (hn : 3 < n) (hne9 : n ≠ 9) (hne16 : n ≠ 16) :
    ∃ p < n, p.Prime ∧ Nat.Prime (((p + 1) * (n - p).totient) ^ 2 + 1)

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

Sources

LeanOeisA233549.conjecture_1 · OeisA233549.conjecture_2 · OeisA233549.conjecture_3

TheoremNumber of primes $p < n$ such that $p \phi(n - p) - 1$ is also prime #

Let $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the primes $p < n$ such that $p \phi(n - p) - 1$ is also prime.

References: - A233566

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

`OeisA233566.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/233566.lean, line 62.

`OeisA233566.conjecture_2`

Open: stated without proof.

Conjecture: For any $n > 2$ there is a prime $p < n$ with $p^2 \phi(n - p) - 1$ prime.

theorem conjecture_2 (n : ℕ) (hn : 2 < n) :
    ∃ p < n, p.Prime ∧ Nat.Prime (p ^ 2 * (n - p).totient - 1)

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

Sources

LeanOeisA233566.conjecture_1 · OeisA233566.conjecture_2

TheoremValues $m = \sigma(k)$ ($0 < m < 2n$) with $2n - 1 - m$ and $2n - 1 + m$ prime #

Let $\sigma$ denote the sum-of-divisors function. The sequence $a(n)$ counts the integers $0 < m < 2n$ of the form $m = \sigma(k)$ ($k > 0$) such that $2n - 1 - m$ and $2n - 1 + m$ are both prime.

References: - A233864

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

`OeisA233864.conjecture_1`

Open: stated without proof.

Conjecture (i): $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/233864.lean, line 78.

`OeisA233864.conjecture_2`

Open: stated without proof.

Conjecture (ii): For any even number $2n > 0$, $2n + \sigma(k)$ is prime for some $0 < k < 2n$.

theorem conjecture_2 (n : ℕ) (hn : 0 < n) :
    ∃ k, 0 < k ∧ k < 2 * n ∧ Nat.Prime (2 * n + σ 1 k)

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

Sources

LeanOeisA233864.conjecture_1 · OeisA233864.conjecture_2

TheoremNumber of integers $0 < k < n$ such that $k \phi(n - k) + 1$ is a square #

Let $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the integers $0 < k < n$ such that $k \phi(n - k) + 1$ is a square.

References: - A234246

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

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

`OeisA234246.conjecture_1`

Open: stated without proof.

Conjecture (i): $a(n) > 0$ if $n$ is not a divisor of $6$.

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

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

`OeisA234246.conjecture_2`

Open: stated without proof.

Conjecture (i): The only values of $n$ with $a(n) = 1$ are $4, 5, 8, 9, 12, 13, 24, 33, 49$.

theorem conjecture_2 (n : ℕ) :
    a n = 1 ↔ n ∈ ({4, 5, 8, 9, 12, 13, 24, 33, 49} : Finset ℕ)

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

`OeisA234246.conjecture_3`

Open: stated without proof.

Conjecture (ii): If $n \ge 60$, then $k + \phi(n - k)$ is a square for some $0 < k < n$.

theorem conjecture_3 (n : ℕ) (hn : 60 ≤ n) :
    ∃ k, 0 < k ∧ k < n ∧ IsSquare (k + (n - k).totient)

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

`OeisA234246.conjecture_4`

Open: stated without proof.

Conjecture (ii): If $n > 60$, then $\sigma(k) + \phi(n - k)$ is a square for some $0 < k < n$, where $\sigma(k)$ is the sum of all positive divisors of $k$.

theorem conjecture_4 (n : ℕ) (hn : 60 < n) :
    ∃ k, 0 < k ∧ k < n ∧ IsSquare (σ 1 k + (n - k).totient)

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

`OeisA234246.conjecture_5`

Open: stated without proof.

Conjecture (iii): If $n > 7$ is not equal to $10$ or $20$, then $\phi(k)\phi(n - k) + 1$ is a square for some $0 < k < n$.

theorem conjecture_5 (n : ℕ) (hn : 7 < n) (hne10 : n ≠ 10) (hne20 : n ≠ 20) :
    ∃ k, 0 < k ∧ k < n ∧ IsSquare (k.totient * (n - k).totient + 1)

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

`OeisA234246.conjecture_6`

Open: stated without proof.

Conjecture (iv): If $n > 7$ is not equal to $10$ or $19$, then $(\phi(k) + \phi(n - k)) / 2$ is a triangular number for some $0 < k < n$.

theorem conjecture_6 (n : ℕ) (hn : 7 < n) (hne10 : n ≠ 10) (hne19 : n ≠ 19) :
    ∃ k, 0 < k ∧ k < n ∧ ∃ m : ℕ, k.totient + (n - k).totient = m * (m + 1)

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

Sources

LeanOeisA234246.conjecture_1 · OeisA234246.conjecture_2 · OeisA234246.conjecture_3 · OeisA234246.conjecture_4 · OeisA234246.conjecture_5 · OeisA234246.conjecture_6

TheoremNumber of integers $0 < k < n$ such that $(k + 1)^{\phi(n - k)} + k$ is prime #

For $n \ge 1$, $a(n)$ counts the integers $0 < k < n$ for which $(k + 1)^{\phi(n - k)} + k$ is prime, where $\phi$ is Euler's totient function.

References: - A234360 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.

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

`OeisA234360.conjecture_1`

Open: stated without proof.

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

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

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

`OeisA234360.conjecture_2`

Solved: stated here without proof.

Conjecture (i): For any $n > 5$ there is a positive integer $k < n$ with $(k + 1)^{\phi(n - k) / 2} - k$ prime.

Disproved for $n = 1408$ in the OEIS Open project, see T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941.

theorem conjecture_2 :
    ¬ ∀ n : ℕ, 5 < n →
      ∃ k, 0 < k ∧ k < n ∧
        ∃ p : ℕ, p.Prime ∧ (p + k) ^ 2 = (k + 1) ^ (n - k).totient

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

`OeisA234360.conjecture_3`

Open: stated without proof.

Conjecture (ii): If $n > 1$, then $k(k + 1)^{\phi(n - k)} + 1$ is prime for some $0 < k < n$.

theorem conjecture_3 (n : ℕ) (hn : 1 < n) :
    ∃ k, 0 < k ∧ k < n ∧ Nat.Prime (k * (k + 1) ^ (n - k).totient + 1)

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

`OeisA234360.conjecture_4`

Open: stated without proof.

Conjecture (ii): If $n > 3$, then $k(k + 1)^{\phi(n - k) / 2} - 1$ is prime for some $0 < k < n$.

theorem conjecture_4 (n : ℕ) (hn : 3 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      ∃ p : ℕ, p.Prime ∧ (p + 1) ^ 2 = k ^ 2 * (k + 1) ^ (n - k).totient

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

Sources

LeanOeisA234360.conjecture_1 · OeisA234360.conjecture_2 · OeisA234360.conjecture_3 · OeisA234360.conjecture_4

TheoremSmallest $x$ such that $x \bmod \phi(x) = n$, or $0$ if no such $x$ exists #

For $n \ge 0$, $a(n)$ is the smallest positive integer $x$ such that $x \bmod \phi(x) = n$, or $0$ if no such $x$ exists, where $\phi$ is Euler's totient function.

References: - A234642

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

`OeisA234642.conjecture`

Open: stated without proof.

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

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

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

Sources

LeanOeisA234642.conjecture

TheoremIntegers $0 < k < n$ with $p = k + \mathrm{prime}(n - k)$ and $\mathrm{prime}(p) - p + 1$ prime #

Let $\mathrm{prime}(m)$ denote the $m$-th prime number. The sequence $a(n)$ counts the integers $0 < k < n$ such that $p = k + \mathrm{prime}(n - k)$ and $\mathrm{prime}(p) - p + 1$ are both prime.

References: - A234694

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

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

`OeisA234694.conjecture_1`

Open: stated without proof.

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

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

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

`OeisA234694.conjecture_2`

Open: stated without proof.

Conjecture (i): For any integer $n > 51$ there is a positive integer $k < n$ such that $p = k + \mathrm{prime}(n - k)$ and $\mathrm{prime}(p) + p + 1$ are both prime.

theorem conjecture_2 (n : ℕ) (hn : 51 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      let p := k + Nat.nth Nat.Prime (n - k - 1)
      p.Prime ∧ Nat.Prime (Nat.nth Nat.Prime (p - 1) + p + 1)

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

`OeisA234694.conjecture_3`

Open: stated without proof.

Conjecture (ii): If $n > 9$, then there is a positive integer $k < n$ such that $m - 1$ and $\mathrm{prime}(m) + m$ are both prime, where $m = k + \mathrm{prime}(n - k)$.

theorem conjecture_3 (n : ℕ) (hn : 9 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      let m := k + Nat.nth Nat.Prime (n - k - 1)
      Nat.Prime (m - 1) ∧ Nat.Prime (Nat.nth Nat.Prime (m - 1) + m)

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

`OeisA234694.conjecture_4`

Open: stated without proof.

Conjecture (ii): If $n > 21$, then there is a positive integer $k < n$ such that $m - 1$ and $\mathrm{prime}(m) - m$ are both prime, where $m = k + \mathrm{prime}(n - k)$.

theorem conjecture_4 (n : ℕ) (hn : 21 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      let m := k + Nat.nth Nat.Prime (n - k - 1)
      Nat.Prime (m - 1) ∧ Nat.Prime (Nat.nth Nat.Prime (m - 1) - m)

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

`OeisA234694.conjecture_5`

Open: stated without proof.

Conjecture (iii): If $n > 483$, then for some $0 < k < n$ both $\mathrm{prime}(m) + m$ and $\mathrm{prime}(m) - m$ are prime, where $m = k + \mathrm{prime}(n - k)$.

theorem conjecture_5 (n : ℕ) (hn : 483 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      let m := k + Nat.nth Nat.Prime (n - k - 1)
      Nat.Prime (Nat.nth Nat.Prime (m - 1) + m) ∧
      Nat.Prime (Nat.nth Nat.Prime (m - 1) - m)

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

`OeisA234694.conjecture_6`

Open: stated without proof.

Conjecture (iv): If $n > 3$, then there is a positive integer $k < n$ such that $\mathrm{prime}(k + \mathrm{prime}(n - k)) + 2$ is prime.

theorem conjecture_6 (n : ℕ) (hn : 3 < n) :
    ∃ k, 0 < k ∧ k < n ∧
      let m := k + Nat.nth Nat.Prime (n - k - 1)
      Nat.Prime (Nat.nth Nat.Prime (m - 1) + 2)

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

Sources

LeanOeisA234694.conjecture_1 · OeisA234694.conjecture_2 · OeisA234694.conjecture_3 · OeisA234694.conjecture_4 · OeisA234694.conjecture_5 · OeisA234694.conjecture_6

TheoremNumber of integers $0 < k < n$ such that $p = k + \phi(n - k)$ and $2(n - p) + 1$ are both prime #

Let $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the integers $0 < k < n$ such that $p = k + \phi(n - k)$ and $2(n - p) + 1$ are both prime.

References: - A234809

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

`OeisA234809.conjecture`

Open: stated without proof.

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

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

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

Sources

LeanOeisA234809.conjecture

TheoremNumber of $0 < k < n-2$ with $p = \phi(k) + \phi(n-k)/2 + 1$ and $p_p - p \pm 1$ prime #

Let $\phi$ denote Euler's totient function and $p_m$ denote the $m$-th prime number. The sequence $a(n)$ counts the number of integers $0 < k < n - 2$ such that $p = \phi(k) + \phi(n-k)/2 + 1$, $p_p - p - 1$, and $p_p - p + 1$ are all prime.

References: - A236097

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

`OeisA236097.conjecture`

Open: stated without proof.

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

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

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

Sources

LeanOeisA236097.conjecture

TheoremPrime quadruplets generated by $p = 3\phi(k) + \phi(n-k) - 1$#

Let $\phi$ denote Euler's totient function. The sequence $a(n)$ counts the number of integers $0 < k < n$ such that $p = 3\phi(k) + \phi(n-k) - 1$, $p + 2$, $p + 6$, and $p + 8$ are all prime.

References: - A236511

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

`OeisA236511.conjecture`

Open: stated without proof.

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

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

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

Sources

LeanOeisA236511.conjecture

TheoremOrdered ways to write $2n = p + q$ with $p, q$ and $p_{p+2} + 2$ all prime #

Let $p_k$ denote the $k$-th prime number. The sequence $a(n)$ counts the number of ordered ways to write $2n = p + q$ with $p, q$, and $p_{p+2} + 2$ all prime.

References: - A236566

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

`OeisA236566.conjecture_1`

Open: stated without proof.

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

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

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

`OeisA236566.conjecture_2`

Open: stated without proof.

Conjecture: (ii) If $n > 30$, then $2n + 1$ can be written as $2p + q$ with $p$, $q$ and $\operatorname{prime}(p + 2) + 2$ all prime.

theorem conjecture_2 (n : ℕ) (hn : 30 < n) :
    ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ (Nat.nth Nat.Prime (p + 1) + 2).Prime ∧
      2 * n + 1 = 2 * p + q

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

Sources

LeanOeisA236566.conjecture_1 · OeisA236566.conjecture_2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Triples summing to \(n\) with… to Ordered ways to write $2n = p +…

TheoremTriples summing to \(n\) with \(2m+1\) and \(2m^3+1\) prime#

OeisA230507.conjecture_1

OeisA230507.conjecture_2

Sources

TheoremSmallest \(n\)-th power equal to a sum of consecutive immediately preceding positive \(n\)-th powers#

OeisA230718.conjecture

Sources

TheoremSum of two numbers with prime conditions#

OeisA231201.conjecture

Sources

TheoremWays to write \(n = x + y\) with \(2^x + y(y+1)/2\) prime#

OeisA231577.conjecture

Sources

TheoremSequence designed to show there are infinitely many primes congruent to \(1\) modulo \(4\)#

OeisA231830.conjecture

Sources

TheoremRepresentations with prime conditions#

OeisA232174.conjecture

Sources

TheoremWays to write \(n = x + y\) with \(nx + y\) and \(ny - x\) both prime#

OeisA232194.conjecture_1

OeisA232194.conjecture_2

OeisA232194.conjecture_3

OeisA232194.conjecture_4

OeisA232194.conjecture_5

OeisA232194.conjecture_6

Sources

TheoremLeast \(m > 0\) such that \(\{2^k - k : k = 1, \dots, m\}\) covers all residues modulo \(n\)#

OeisA232616.conjecture_1

OeisA232616.conjecture_2

OeisA232616.conjecture_3

Sources

TheoremRepresentations \(n = k^2 + m\) (\(0 < k^2 \le m\)) with \(\sigma(k^2) + \phi(m)\) prime#

OeisA233544.conjecture_1

OeisA233544.conjecture_2

OeisA233544.conjecture_3

Sources

TheoremNumber of ways to write \(n = p + q\) (\(q > 0\)) with \(p\) and \((\phi(p)\phi(q))^4 + 1\) prime#

OeisA233549.conjecture_1

OeisA233549.conjecture_2

OeisA233549.conjecture_3

Sources

TheoremNumber of primes \(p < n\) such that \(p \phi(n - p) - 1\) is also prime#

OeisA233566.conjecture_1

OeisA233566.conjecture_2

Sources

TheoremValues \(m = \sigma(k)\) (\(0 < m < 2n\)) with \(2n - 1 - m\) and \(2n - 1 + m\) prime#

OeisA233864.conjecture_1

OeisA233864.conjecture_2

Sources

TheoremNumber of integers \(0 < k < n\) such that \(k \phi(n - k) + 1\) is a square#

OeisA234246.conjecture_1

OeisA234246.conjecture_2

OeisA234246.conjecture_3

OeisA234246.conjecture_4

OeisA234246.conjecture_5

OeisA234246.conjecture_6

Sources

TheoremNumber of integers \(0 < k < n\) such that \((k + 1)^{\phi(n - k)} + k\) is prime#

OeisA234360.conjecture_1

OeisA234360.conjecture_2

OeisA234360.conjecture_3

OeisA234360.conjecture_4

Sources

TheoremSmallest \(x\) such that \(x \bmod \phi(x) = n\), or \(0\) if no such \(x\) exists#

OeisA234642.conjecture

Sources

TheoremIntegers \(0 < k < n\) with \(p = k + \mathrm{prime}(n - k)\) and \(\mathrm{prime}(p) - p + 1\) prime#

OeisA234694.conjecture_1

OeisA234694.conjecture_2

OeisA234694.conjecture_3

OeisA234694.conjecture_4

OeisA234694.conjecture_5

OeisA234694.conjecture_6

Sources

TheoremNumber of integers \(0 < k < n\) such that \(p = k + \phi(n - k)\) and \(2(n - p) + 1\) are both prime#

OeisA234809.conjecture

Sources

TheoremNumber of \(0 < k < n-2\) with \(p = \phi(k) + \phi(n-k)/2 + 1\) and \(p_p - p \pm 1\) prime#

TheoremTriples summing to \(n\) with \(2m+1\) and \(2m^3+1\) prime #

`OeisA230507.conjecture_1`

`OeisA230507.conjecture_2`

TheoremSmallest \(n\)-th power equal to a sum of consecutive immediately preceding positive \(n\)-th powers #

`OeisA230718.conjecture`

TheoremSum of two numbers with prime conditions #

`OeisA231201.conjecture`

TheoremWays to write \(n = x + y\) with \(2^x + y(y+1)/2\) prime #

`OeisA231577.conjecture`

`OeisA231830.conjecture`

TheoremRepresentations with prime conditions #

`OeisA232174.conjecture`

TheoremWays to write \(n = x + y\) with \(nx + y\) and \(ny - x\) both prime #

`OeisA232194.conjecture_1`

`OeisA232194.conjecture_2`

`OeisA232194.conjecture_3`

`OeisA232194.conjecture_4`

`OeisA232194.conjecture_5`

`OeisA232194.conjecture_6`

`OeisA232616.conjecture_1`

`OeisA232616.conjecture_2`

`OeisA232616.conjecture_3`

TheoremRepresentations \(n = k^2 + m\) (\(0 < k^2 \le m\)) with \(\sigma(k^2) + \phi(m)\) prime #

`OeisA233544.conjecture_1`

`OeisA233544.conjecture_2`

`OeisA233544.conjecture_3`

TheoremNumber of ways to write \(n = p + q\) (\(q > 0\)) with \(p\) and \((\phi(p)\phi(q))^4 + 1\) prime #

`OeisA233549.conjecture_1`

`OeisA233549.conjecture_2`

`OeisA233549.conjecture_3`

TheoremNumber of primes \(p < n\) such that \(p \phi(n - p) - 1\) is also prime #

`OeisA233566.conjecture_1`

`OeisA233566.conjecture_2`

TheoremValues \(m = \sigma(k)\) (\(0 < m < 2n\)) with \(2n - 1 - m\) and \(2n - 1 + m\) prime #

`OeisA233864.conjecture_1`

`OeisA233864.conjecture_2`

TheoremNumber of integers \(0 < k < n\) such that \(k \phi(n - k) + 1\) is a square #

`OeisA234246.conjecture_1`

`OeisA234246.conjecture_2`

`OeisA234246.conjecture_3`

`OeisA234246.conjecture_4`

`OeisA234246.conjecture_5`

`OeisA234246.conjecture_6`

TheoremNumber of integers \(0 < k < n\) such that \((k + 1)^{\phi(n - k)} + k\) is prime #

`OeisA234360.conjecture_1`

`OeisA234360.conjecture_2`

`OeisA234360.conjecture_3`

`OeisA234360.conjecture_4`

TheoremSmallest \(x\) such that \(x \bmod \phi(x) = n\), or \(0\) if no such \(x\) exists #

`OeisA234642.conjecture`

TheoremIntegers \(0 < k < n\) with \(p = k + \mathrm{prime}(n - k)\) and \(\mathrm{prime}(p) - p + 1\) prime #

`OeisA234694.conjecture_1`

`OeisA234694.conjecture_2`

`OeisA234694.conjecture_3`

`OeisA234694.conjecture_4`

`OeisA234694.conjecture_5`

`OeisA234694.conjecture_6`

TheoremNumber of integers \(0 < k < n\) such that \(p = k + \phi(n - k)\) and \(2(n - p) + 1\) are both prime #

`OeisA234809.conjecture`

TheoremNumber of \(0 < k < n-2\) with \(p = \phi(k) + \phi(n-k)/2 + 1\) and \(p_p - p \pm 1\) prime #

`OeisA236097.conjecture`

`OeisA236511.conjecture`

TheoremOrdered ways to write \(2n = p + q\) with \(p, q\) and \(p_{p+2} + 2\) all prime #

`OeisA236566.conjecture_1`

`OeisA236566.conjecture_2`