Primes of the form $3^n \pm 3^k… to Primes \(p < n\) with $n^2 - n +…
TheoremPrimes of the form \(3^n \pm 3^k \pm 1\)#
Number of primes of the form \(3^n \pm 3^k \pm 1\) with \(0 \le k < n\).
References: - A196698
Quoted from FormalConjectures/OEIS/196698.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.
OeisA196698.conjecture_1
Open: stated without proof.
"Conjecture: all elements of this sequence are greater than \(0\)."
theorem conjecture_1 (n : ℕ) (hn : 1 ≤ n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/196698.lean, line 66.
OeisA196698.conjecture_2
Open: stated without proof.
"I conjecture the contrary: infinitely many elements of this sequence are equal to \(0\)." - Charles R Greathouse IV, Nov 21 2011
theorem conjecture_2 : Set.Infinite {n : ℕ | a n = 0}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/196698.lean, line 74.
Sources
TheoremLerch quotients of odd primes#
The Lerch quotient of an odd prime \(p\) is given by
\[L_p = \frac{\left(\sum_{k=1}^{p-1} q_p(k)\right) - w_p}{p}\]where \(q_p(k) = (k^{p-1}-1)/p\) is the Fermat quotient and \(w_p = ((p-1)!+1)/p\) is the Wilson quotient. For \(n > 1\), \(a(n)\) is the Lerch quotient of the \(n\)-th prime \(p_n\).
References: - A197630
Quoted from FormalConjectures/OEIS/197630.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.
OeisA197630.conjecture
Open: stated without proof.
"Is \(13\) the only Lerch quotient that is itself prime?"
theorem conjecture : ∀ n : ℕ, 1 < n → (a n).Prime → a n = 13
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/197630.lean, line 87.
Sources
TheoremPosition of \(n\)-th partial sum of the harmonic series when jointly ranked with \(\{\log(k+1)\}\)#
Position of \(n\)-th partial sum of the harmonic series when all the partial sums are jointly ranked with the set \(\{\log(k+1)\}\); complement of A206912.
References: - A206911 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.
Quoted from FormalConjectures/OEIS/206911.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.
OeisA206911.conjecture_1
Solved: stated here without proof.
"Conjecture: the difference sequence of A206911 consists of \(2\)s and \(3\)s." - Clark Kimberling, Feb 13 2012
Proved 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 : ℕ) (hn : 1 ≤ n) : diff n = 2 ∨ diff n = 3
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/206911.lean, line 179.
OeisA206911.conjecture_2
Solved: stated here without proof.
"Conjecture: the ratio (number of \(3\)s)/(number of \(2\)s) tends to a number between \(3.5\) and \(3.6\)." - Clark Kimberling, Feb 13 2012
Proved 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 :
∃ l : ℝ, 3.5 < l ∧ l < 3.6 ∧
Filter.Tendsto (fun N : ℕ => (count3 N : ℝ) / (count2 N : ℝ)) Filter.atTop (nhds l)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/206911.lean, line 190.
Sources
TheoremExpansion of \(\sum_{n \ge 0} \frac{(3n)!}{n!^3} \frac{x^{2n}}{(1-x)^{3n+1}}\)#
The sequence \(a(n)\) given by the expansion of \(\sum_{n \ge 0} \frac{(3n)!}{n!^3} \frac{x^{2n}}{(1-x)^{3n+1}}\), which satisfies
\[a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n-k}{k} \binom{n+k}{k}.\]References: - A208425
Quoted from FormalConjectures/OEIS/208425.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.
OeisA208425.conjecture_1
Open: stated without proof.
Conjecture (i): For any prime \(p > 3\) and positive integer \(n\), the number \((a(pn)-a(n))/(pn)^3\) is always a \(p\)-adic integer. - Zhi-Wei Sun, Nov 12 2016
theorem conjecture_1 (p : ℕ) (hp : p.Prime) (hpgt3 : 3 < p) (n : ℕ) (hn : 0 < n) :
0 ≤ padicValRat p (((a (p * n) : ℚ) - (a n : ℚ)) / ((p * n : ℚ) ^ 3))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/208425.lean, line 61.
OeisA208425.conjecture_2
Open: stated without proof.
Conjecture (ii), part 1: For any prime \(p \equiv 1 \pmod{3}\), we have \(\sum_{k=0}^{p-1} a(k) \equiv \binom{2(p-1)/3}{(p-1)/3} \pmod{p^2}\). - Zhi-Wei Sun, Nov 12 2016
theorem conjecture_2 (p : ℕ) (hp : p.Prime) (hmod : p % 3 = 1) :
(∑ k ∈ Finset.range p, a k) % (p ^ 2) =
((2 * (p - 1) / 3).choose ((p - 1) / 3)) % (p ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/208425.lean, line 71.
OeisA208425.conjecture_3
Open: stated without proof.
Conjecture (ii), part 2: For any prime \(p \equiv 2 \pmod{3}\), we have \(\sum_{k=0}^{p-1} a(k) \equiv \frac{2p}{\binom{2(p+1)/3}{(p+1)/3}} \pmod{p^2}\). - Zhi-Wei Sun, Nov 12 2016
theorem conjecture_3 (p : ℕ) (hp : p.Prime) (hmod : p % 3 = 2) :
((∑ k ∈ Finset.range p, (a k : ℚ)) -
(2 * p : ℚ) / ((2 * (p + 1) / 3).choose ((p + 1) / 3) : ℚ)).num % (p ^ 2 : ℤ) = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/208425.lean, line 82.
Sources
TheoremLeast integer \(m > 1\) dividing no sum of two distinct primorials up to \(P_n\)#
For \(n \ge 1\), \(a(n)\) is the least integer \(m > 1\) such that \(m\) divides none of \(P_i + P_j\) with \(0 < i < j \le n\), where \(P_k\) is the product of the first \(k\) primes.
References: - A210186
Quoted from FormalConjectures/OEIS/210186.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.
OeisA210186.conjecture_1
Open: stated without proof.
"Conjecture: all the terms are primes." - Zhi-Wei Sun, Mar 18 2012
theorem conjecture_1 (n : ℕ) (hn : 1 ≤ n) : (a n).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/210186.lean, line 123.
OeisA210186.conjecture_2
Open: stated without proof.
"Conjecture: \(a(n) < n^2\) for all \(n > 1\)." - Zhi-Wei Sun, Mar 18 2012
theorem conjecture_2 (n : ℕ) (hn : 1 < n) : a n < n ^ 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/210186.lean, line 131.
Sources
TheoremIntegrality and supercongruences of the factorial ratio \(\frac{(6n)! n!}{(3n)! (2n)!^2}\)#
Integral factorial ratio sequence:
\[a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}\]References: - A211417 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - [Me11] R. Meštrović, Wolstenholme's theorem: Its Generalizations and Extensions in the last hundred and fifty years (1862-2012), arXiv:1111.3057 (2011).
Quoted from FormalConjectures/OEIS/211417.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 7 solved. It also has 5 test statements, counted here but not shown.
OeisA211417.thirty_mul_sub_one_dvd_a
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/211417.wip.lean#L243.
It appears that \(a(n)/(30n - 1)\) is integral for all \(n\) (checked up to \(n = 1000\)). - Peter Bala, Aug 28 2025
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem thirty_mul_sub_one_dvd_a (n : ℕ) : (30 * (n : ℤ) - 1) ∣ (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 85.
OeisA211417.seven_mul_a_dvd_two_mul_add_one
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L866-L868.
Conjecture: "7a(n)/(2n + 1) ... [is an] integer for all n (checked up to n = 1000)." - Peter Bala, Aug 28 2025
theorem seven_mul_a_dvd_two_mul_add_one (n : ℕ) :
(2 * (n : ℤ) + 1) ∣ 7 * (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 96.
OeisA211417.a_dvd_three_mul_add_one
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1173-L1175.
Conjecture: "a(n)/(3*n + 1) ... [is an] integer for all n (checked up to n = 1000)." - Peter Bala, Aug 28 2025
theorem a_dvd_three_mul_add_one (n : ℕ) :
(3 * (n : ℤ) + 1) ∣ (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 108.
OeisA211417.a_dvd_five_mul_add_one
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1446-L1448.
Conjecture: "a(n)/(5*n + 1) ... [is an] integer for all n (checked up to n = 1000)." - Peter Bala, Aug 28 2025
theorem a_dvd_five_mul_add_one (n : ℕ) :
(5 * (n : ℤ) + 1) ∣ (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 120.
OeisA211417.forty_two_mul_a_dvd_product
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a211417/blob/cad1fb228b5b80573cab3eeb92c8be57fd73c506/lean/OeisA211417FC.lean#L1514-L1524.
Conjecture: "42a(n)/((2n + 1)(3n + 1)(5n + 1)) [is an] integer for all n (checked up to n = 1000)." - Peter Bala, Aug 28 2025
theorem forty_two_mul_a_dvd_product (n : ℕ) :
((2 * (n : ℤ) + 1) * (3 * (n : ℤ) + 1) * (5 * (n : ℤ) + 1)) ∣
42 * (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 132.
OeisA211417.general_divisibility
Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/fbc6706451b0e80787580d91ee6c252c121e0165/FormalConjectures/OEIS/211417.lean#L555.
Conjecture: "More generally, for r >= 1, we conjecture that there exists a constant D(r) such that D(r)a(n)/Product_{i = 1..r, i coprime to 30} (30n - i) is integral for all n." - Peter Bala, Aug 28 2025
This generalizes
thirty_mul_sub_one_dvd_a(the \(r = 1\) case where \(D(1) = 1\)).Proof sketch (kernel-checked development at the
formal_proofpermalink below, which proves the non-vacuous form with the explicit positive witness \(D = (r!)^{r^2}\)): Legendre-valuation analysis of the Landau step function \(\Delta(x) = \lfloor 30x \rfloor + \lfloor x \rfloor - \lfloor 15x \rfloor - \lfloor 10x \rfloor - \lfloor 6x \rfloor\), whose values lie in \(\{0, 1\}\). Three ingredients: a unit-class rigidity lemma (\(\Delta_c = 1\) for every unit class \(c\) modulo \(30\)), a witness-uniqueness bound for prime powers \(p^k > r\) (at most one factor of the divisor product is divisible by \(p^k\)), and a uniform low-layer budget for \(p^k \le r\) absorbed by the witness constant.
theorem general_divisibility (r : ℕ) (hr : 1 ≤ r) :
∃ D : ℤ, 0 < D ∧ ∀ n : ℕ, (divisorProduct n r) ∣ (D * (a n : ℤ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 157.
OeisA211417.supercongruence
Solved: stated here; a Lean proof is at https://github.com/niketp03/atlas-fc-verified/blob/15e4b3a7584e218cec531aeaf71cce72a8a9ecb1/AtlasFCSolutions/OeisA211417.lean#L848.
Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive integer k." - Peter Bala, Jan 24 2020
More generally, "the congruences a(np^k) == a(np^(k-1)) ( mod p^(3*k) ) may hold for any prime p >= 5 and any positive integers n and k."
The same OEIS comment (Peter Bala, Jan 24 2020) already sketches an informal proof of the supercongruence: write \(a(n) = \binom{30n}{15n}\binom{15n}{5n} / \binom{6n}{n}\) and apply [Me11, eq. (39), p. 12].
Solved: a Lean 4 proof, derived from the Atlas proofs in facebookresearch/atlas-lean, is linked in
formal_proof.
theorem supercongruence (p k : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) (hk : 0 < k) :
(p : ℤ) ^ (3 * k) ∣ ((a (p ^ k) : ℤ) - (a (p ^ (k - 1)) : ℤ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211417.lean, line 180.
Sources
TheoremSequence \(\frac{(8n)! n!}{(4n)! (3n)! (2n)!}\)#
The sequence \(a(n) = \frac{(8n)! n!}{(4n)! (3n)! (2n)!}\), which is always an integer for \(n \ge 0\).
References: - A211420 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026. - OEIS-A211420 by Ansh Mishra and Aryan Senthilkumar (2026)
Quoted from FormalConjectures/OEIS/211420.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 solved. It also has 5 test statements, counted here but not shown.
OeisA211420.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L25-L28.
"It appears that \(35 \cdot a(n)/(n + 1)\) is an integer for all \(n\)." - Peter Bala, Aug 26 2025
Proved and formalized in Lean 4 by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_1 (n : ℕ) : (n + 1) ∣ 35 * a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 70.
OeisA211420.conjecture_2
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L25-L28.
"It appears that \(3 \cdot a(n)/(2n + 1)\) is an integer for all \(n\)." - Peter Bala, Aug 26 2025
Proved and formalized in Lean 4 by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_2 (n : ℕ) : (2 * n + 1) ∣ 3 * a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 83.
OeisA211420.conjecture_3
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L25-L28.
"It appears that \(5 \cdot a(n)/(3n + 1)\) is an integer for all \(n\)." - Peter Bala, Aug 26 2025
Follows from a result of Z.-W. Sun (2012), and formalized in Lean 4 by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_3 (n : ℕ) : (3 * n + 1) ∣ 5 * a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 97.
OeisA211420.conjecture_4
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L30-L33.
"More generally, we conjecture that there are constants \(C(k, r) > 0\), \(k = 1, 2\) or \(3\), \(r \ge 1\), such that \(a(n) \cdot C(k, r)/((kn + 1)(kn + 2)\cdots(kn + r))\) is an integer for all \(n\)." - Peter Bala, Aug 26 2025
Proved and formalized in Lean 4 by DannyExperiments (2026) and independently by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_4 (k r : ℕ) (hk : k = 1 ∨ k = 2 ∨ k = 3) (hr : 1 ≤ r) :
∃ C : ℕ, 0 < C ∧ ∀ n : ℕ, (k * n + 1).ascFactorial r ∣ C * a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 112.
OeisA211420.conjecture_5
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L35-L38.
"It also appears that \(a(n)\) is divisible by \(8n - 1\) for all \(n\)." - Peter Bala, Aug 26 2025
Proved and formalized in Lean 4 by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_5 (n : ℕ) :
((8 * n : ℤ) - 1) ∣ (a n : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 126.
OeisA211420.conjecture_6
Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A211420/blob/2bd4dbf1185a9fa8edc2cb9a61d471583d018d08/lean/DMSolutions/OEIS_A211420/Solution.lean#L40-L43.
"More generally, we conjecture that there are constants \(K(r) > 0\), \(r \ge 0\), such that \(a(n) \cdot K(r)/((8n - 1)(8n - 3)\cdots(8n - (2r+1)))\) is an integer for all \(n\)." - Peter Bala, Aug 26 2025
Proved in the OEIS Open project, see T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941, and also by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_6 (r : ℕ) :
∃ K : ℤ, 0 < K ∧ ∀ n : ℕ, oddDescendingProduct n r ∣ (a n : ℤ) * K
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/211420.lean, line 143.
Sources
TheoremBalanced walks on a 4-dimensional cubic lattice with neighbor steps#
The sequence \(a(n)\) counts the words over a \(4\)-ary alphabet (either empty or starting with the first letter) in which each letter occurs \(n\) times and adjacent letters are equal or adjacent in the alphabet. Equivalently,
\[a(n) = \sum_{k=0}^{n-1} \binom{n}{k} \binom{n-1}{k} \binom{n+k-1}{k}^2\]for \(n \ge 1\) and \(a(0) = 1\).
References: - A212334
Quoted from FormalConjectures/OEIS/212334.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.
OeisA212334.conjecture_1
Open: stated without proof.
"It appears that for primes \(p \ge 5\), \(a(p) \equiv 1 \pmod{p^5}\)." - Peter Bala, Dec 12 2021
theorem conjecture_1 (p : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) :
a p % (p ^ 5) = 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212334.lean, line 66.
OeisA212334.conjecture_2
Open: stated without proof.
"Conjecture: for \(r \ge 2\), and all primes \(p \ge 5\), \(a(p^r) \equiv a(p^{r-1}) \pmod{p^{3r+3}}\)." - Peter Bala, Oct 13 2022
theorem conjecture_2 (p r : ℕ) (hp : p.Prime) (hp5 : 5 ≤ p) (hr2 : 2 ≤ r) :
a (p ^ r) % (p ^ (3 * r + 3)) = a (p ^ (r - 1)) % (p ^ (3 * r + 3))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212334.lean, line 76.
Sources
TheoremPartial sums of \((-1)^{k - \Omega(k)}\)#
The sequence \(a(n) = \sum_{k=1}^n (-1)^{k - \Omega(k)}\), where \(\Omega(k)\) is the total number of prime factors of \(k\) counted with multiplicity.
References: - A212496
Quoted from FormalConjectures/OEIS/212496.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.
OeisA212496.conjecture_1
Open: stated without proof.
"On May 16 2012, Zhi-Wei Sun conjectured that \(a(n)\) is positive for each \(n > 4\)." - Zhi-Wei Sun, May 19 2012
theorem conjecture_1 (n : ℕ) (hn : 4 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 69.
OeisA212496.conjecture_2
Open: stated without proof.
"Moreover, he guessed that \(a(n) > \sqrt{n}\) for any \(n > 324\)." - Zhi-Wei Sun, May 19 2012
theorem conjecture_2 (n : ℕ) (hn : 324 < n) :
Real.sqrt (n : ℝ) < (a n : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 77.
OeisA212496.conjecture_3
Open: stated without proof.
"He also guessed that \(a(n) < \sqrt{n}\log(\log(n))\) for \(n > 5892\)." - Zhi-Wei Sun, May 19 2012
theorem conjecture_3 (n : ℕ) (hn : 5892 < n) :
(a n : ℝ) < Real.sqrt (n : ℝ) * Real.log (Real.log (n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 86.
OeisA212496.conjecture_4
Open: stated without proof.
"Sun also conjectured that \(b(n) = \sum_{k=1}^n (-1)^{k-\Omega(k)}/k < 0\) for all \(n=1,2,3,\dots\)" - Zhi-Wei Sun, May 19 2012
theorem conjecture_4 (n : ℕ) (hn : 0 < n) : b n < 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 95.
OeisA212496.conjecture_5
Open: stated without proof.
"Moreover, he guessed that \(b(n) < -1/\sqrt{n}\) for all \(n > 1\)." - Zhi-Wei Sun, May 19 2012
theorem conjecture_5 (n : ℕ) (hn : 1 < n) :
(b n : ℝ) < -1 / Real.sqrt (n : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 103.
OeisA212496.conjecture_6
Open: stated without proof.
"He also guessed that \(b(n) > -\log(\log(n))/\sqrt{n}\) for \(n > 2008\)." - Zhi-Wei Sun, May 19 2012
theorem conjecture_6 (n : ℕ) (hn : 2008 < n) :
-Real.log (Real.log (n : ℝ)) / Real.sqrt (n : ℝ) < (b n : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212496.lean, line 112.
Sources
TheoremRemainder of \(2^{n+2}\) modulo \(n\)#
The sequence \(a(n) = 2^{n+2} \bmod n\).
References: - A212844
Quoted from FormalConjectures/OEIS/212844.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.
OeisA212844.conjecture
Open: stated without proof.
"Conjecture: every integer \(k \ge 0\) appears in \(a(n)\) at least once."
theorem conjecture (k : ℕ) : ∃ n : ℕ, 1 ≤ n ∧ a n = k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/212844.lean, line 56.
Sources
TheoremTwin primes of the form \((3^n - k) 2^n \pm 1\)#
For \(n > 0\), \(a(n)\) is the smallest nonnegative integer \(k\) such that \((3^n - k) 2^n - 1\) and \((3^n - k) 2^n + 1\) form a twin prime pair.
References: - A214497
Quoted from FormalConjectures/OEIS/214497.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.
OeisA214497.conjecture
Open: stated without proof.
Conjecture: There is always one such \(k\) for each \(n > 0\) such that \((3^n - k) 2^n - 1\) and \((3^n - k) 2^n + 1\) are a twin prime pair.
theorem conjecture (n : ℕ) (hn : 0 < n) : (a n).isSome
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/214497.lean, line 78.
Sources
TheoremNumber of \(0\)'s in the binary expansion of \(n^2\)#
For \(n \ge 0\), \(a(n)\) is the number of \(0\)'s in the base-\(2\) representation of \(n^2\) (with \(a(0) = 1\)).
References: - A214560
Quoted from FormalConjectures/OEIS/214560.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.
OeisA214560.conjecture
Open: stated without proof.
Conjecture: For every \(x \ge 0\), there is an \(i\) such that \(a(n) > x\) for all \(n > i\).
theorem conjecture (x : ℕ) : ∃ i : ℕ, ∀ n > i, x < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/214560.lean, line 58.
Sources
TheoremSmallest deficient multiplier for non-deficiency#
For \(n \ge 2\), \(a(n)\) is the smallest deficient number \(k\) such that the product \(k \cdot n\) is non-deficient (i.e., perfect or abundant).
References: - A215926
Quoted from FormalConjectures/OEIS/215926.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.
OeisA215926.conjecture_1
Open: stated without proof.
Conjecture: For every \(n \ge 2\), \(a(n)\) is \(1\), \(3\), or a power of \(2\).
theorem conjecture_1 (n : ℕ) (hn : 2 ≤ n) :
a n = 1 ∨ a n = 3 ∨ (a n).isPowerOfTwo
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/215926.lean, line 66.
OeisA215926.conjecture_2
Open: stated without proof.
Conjecture: The first occurrence of \(2^m\) happens at A014210\((m)\).
We require \(m \ge 1\) because for \(m = 0\), the first occurrence of \(2^0 = 1\) is at \(n = 6\), whereas \(\mathrm{A014210}(0) = 2\) gives \(a(2) = 3\).
theorem conjecture_2 (m : ℕ) (hm : 1 ≤ m) :
IsLeast {n : ℕ | 2 ≤ n ∧ a n = 2 ^ m} (nextPrimeTwoPow m)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/215926.lean, line 77.
Sources
TheoremNumber of primes between \(n^3 - n\) and \(n^3\)#
For \(n \ge 1\), \(a(n)\) is the number of primes \(p\) satisfying \(n^3 - n < p \le n^3\), given by \(\pi(n^3) - \pi(n^3 - n)\).
References: - A216265
Quoted from FormalConjectures/OEIS/216265.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.
OeisA216265.conjecture
Open: stated without proof.
Conjecture: For every \(n > 13\), \(a(n) > 0\).
theorem conjecture (n : ℕ) (hn : 13 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/216265.lean, line 105.
Sources
TheoremNumber of primes between \(n^2\) and \(n^2 + (\log_2 n)^2\)#
For \(n \ge 1\), \(a(n)\) is the number of primes between \(n^2\) and \(n^2 + (\log_2 n)^2\) inclusive, given by \(\pi(\lfloor n^2 + (\log_2 n)^2 \rfloor) - \pi(n^2)\).
References: - A217317
Quoted from FormalConjectures/OEIS/217317.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.
OeisA217317.conjecture
Open: stated without proof.
Conjecture: For every \(n > 4765516\), \(a(n) > 0\).
theorem conjecture (n : ℕ) (hn : 4765516 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/217317.lean, line 115.
Sources
TheoremRecurrence \(a(n+1) = 2n(n+1)a(n) - n^4 a(n-1)\) and associated polynomials#
The sequence \(a(n)\) is defined by \(a(0) = 1\), \(a(1) = 0\), and \(a(n+1) = 2n(n+1)a(n) - n^4 a(n-1)\) for \(n > 0\). The associated polynomials \(S_n(x) \in \mathbb{Z}[x]\) satisfy \(S_0(x) = 1\), \(S_1(x) = x\), and \(S_{n+1}(x) = (x + 2n(n+1)) S_n(x) - n^4 S_{n-1}(x)\) for \(n > 0\).
References: - A217703 - Sun-Conjectures-ii-iii- by Ansh Mishra and Aryan Senthilkumar (2026)
Quoted from FormalConjectures/OEIS/217703.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 and 2 solved. It also has 5 test statements, counted here but not shown.
OeisA217703.conjecture_1
Open: stated without proof.
Conjecture, (i): \(S_n(x)\) is irreducible over the field of rational numbers for every \(n = 1, 2, 3, \dots\) - Zhi-Wei Sun, Mar 20 2013
theorem conjecture_1 (n : ℕ) (hn : 1 ≤ n) :
Irreducible (Polynomial.map (Int.castRingHom ℚ) (polyS n))
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/217703.lean, line 78.
OeisA217703.conjecture_2
Solved: stated here without proof.
Conjecture, (ii): \(a(n) = S_n(0)\) is negative if and only if \(1 < n < 58\) or \(n > 2177\). - Zhi-Wei Sun, Mar 20 2013
Disproved by Ansh Mishra and Aryan Senthilkumar: \(a(81935) > 0\).
theorem conjecture_2 :
¬ ∀ n : ℕ, (a n < 0 ↔ (1 < n ∧ n < 58) ∨ 2177 < n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/217703.lean, line 90.
OeisA217703.conjecture_3
Solved: stated here; a Lean proof is at https://github.com/anshM123/Sun-Conjectures-ii-iii-/blob/7016c789cbe3b36aff4a5bcaa3ece16ea9331f8e/lean/DMSolutions/OEIS_A217703/Solution.lean#L19-L23.
Conjecture, (iii): \(|a(n)|^{1/n} = o(n^2)\) as \(n\) tends to infinity. - Zhi-Wei Sun, Mar 20 2013
Disproved and formalized in Lean 4 by Ansh Mishra and Aryan Senthilkumar (with Claude).
theorem conjecture_3 :
¬ Filter.Tendsto (fun n : ℕ => |(a n : ℝ)| ^ (1 / (n : ℝ)) / (n : ℝ) ^ 2)
Filter.atTop (nhds 0)
Category research solved; AMS 11 Number theory, 26 Real functions. Declared in FormalConjectures/OEIS/217703.lean, line 104.
Sources
TheoremSmallest integer \(s > n\) such that \(1 + 2s + 3s^2 + \dots + n s^{n-1}\) is prime#
For \(n \ge 2\), \(a(n)\) is the smallest integer \(s > n\) such that the sum \(P_n(s) = \sum_{k=0}^{n-1} (k+1) s^k\) is a prime number.
References: - A217785
Quoted from FormalConjectures/OEIS/217785.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 4 open. It also has 5 test statements, counted here but not shown.
OeisA217785.conjecture_1
Open: stated without proof.
Conjecture: For each \(n \ge 2\), there are infinitely many primes of the form \(1 + 2s + \dots + n s^{n-1}\) where \(s\) is a positive integer.
theorem conjecture_1 (n : ℕ) (hn : 2 ≤ n) :
{s : ℕ | 0 < s ∧ Nat.Prime (polyP n s)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/217785.lean, line 101.
OeisA217785.conjecture_2
Open: stated without proof.
Conjecture: For each \(n \ge 2\), \(a(n) < 12 n^2\).
theorem conjecture_2 (n : ℕ) (hn : 2 ≤ n) :
∃ m < 12 * n ^ 2, a n = some m
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/217785.lean, line 109.
OeisA217785.conjecture_3
Open: stated without proof.
Conjecture: The polynomials \(s_n(x) = \sum_{k=0}^n (k+1) x^k\) for \(n \ge 1\) are all irreducible over the field of rational numbers.
theorem conjecture_3 (n : ℕ) (hn : 1 ≤ n) :
Irreducible (Polynomial.map (Int.castRingHom ℚ) (polyS n))
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/217785.lean, line 118.
OeisA217785.conjecture_4
Open: stated without proof.
Conjecture: For \(n \ge 1\), the polynomial \(s_n(x) = \sum_{k=0}^n (k+1) x^k\) is reducible modulo every prime if and only if \(n\) has the form \(8k(k+1)\) where \(k\) is a positive integer.
theorem conjecture_4 (n : ℕ) (hn : 1 ≤ n) :
(∀ p : ℕ, p.Prime → ¬ Irreducible (Polynomial.map (Int.castRingHom (ZMod p)) (polyS n))) ↔
∃ k : ℕ, 0 < k ∧ n = 8 * k * (k + 1)
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/217785.lean, line 128.
Sources
TheoremPartitions \(n = x + y\) with \(x^2 + xy + y^2\) prime#
For \(n \ge 1\), \(a(n)\) is the number of ways to write \(n\) as \(x + y\) with \(0 < x \le y\) such that \(x^2 + xy + y^2\) is prime.
References: - A218585 - E. Hecke, "Eine neue Art von Zetafunktionen und ihre Beziehungen zur Verteilung der Primzahlen. Zweite Mitteilung", Math. Z. 6 (1920), 11–51.
Quoted from FormalConjectures/OEIS/218585.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: 2 open and 2 solved. It also has 6 test statements, counted here but not shown.
OeisA218585.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\) with the only exception \(n = 8\).
theorem conjecture_1 (n : ℕ) (hn : 1 < n) (h8 : n ≠ 8) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218585.lean, line 76.
OeisA218585.conjecture_2
Open: stated without proof.
Conjecture: The number of primes of the form \(nx + (n - x)^2\) with \(0 < x < n / 3\) is positive for \(n > 12\). - Zak Seidov, Sep 25 2013
theorem conjecture_2 (n : ℕ) (hn : 12 < n) :
∃ x : ℕ, 0 < x ∧ 3 * x < n ∧ Nat.Prime (n * x + (n - x) ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218585.lean, line 85.
OeisA218585.conjecture_3
Solved: stated here without proof.
\[\lim_{N \to \infty} \frac{\sum_{p < N, \, p \equiv 1 \pmod 3} x(p)}{\sum_{p < N, \, p \equiv 1 \pmod 3} y(p)} = 1 + \sqrt{3},\]where for a prime \(p \equiv 1 \pmod 3\), \(x(p) > y(p) > 0\) are the unique positive integers such that \(p = x(p)^2 + x(p)y(p) + y(p)^2\). - Zhi-Wei Sun
This follows from Hecke's (1920) equidistribution theorem for Hecke Grossencharacters of \(\mathbb{Q}(\sqrt{-3})\) and partial summation with the prime number theorem.
theorem conjecture_3 :
Filter.atTop.Tendsto
(fun N : ℕ =>
(∑ p ∈ (Finset.range N).filter (fun p => p.Prime ∧ p % 3 = 1), (xp p : ℝ)) /
(∑ p ∈ (Finset.range N).filter (fun p => p.Prime ∧ p % 3 = 1), (yp p : ℝ)))
(nhds (1 + Real.sqrt 3))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218585.lean, line 99.
OeisA218585.conjecture_4
Solved: stated here without proof.
Conjecture:
\[\lim_{N \to \infty} \frac{\sum_{p < N, \, p \equiv 1 \pmod 3} x(p)^2}{\sum_{p < N, \, p \equiv 1 \pmod 3} y(p)^2} = \frac{52}{9},\]where for a prime \(p \equiv 1 \pmod 3\), \(x(p) > y(p) > 0\) are the unique positive integers such that \(p = x(p)^2 + x(p)y(p) + y(p)^2\). - Zhi-Wei Sun
Disproved by Hecke's (1920) equidistribution theorem for Hecke Grossencharacters of \(\mathbb{Q}(\sqrt{-3})\), which yields the true limit
\[\frac{\int_0^{\pi/6} (\cos\theta - \frac{1}{\sqrt{3}}\sin\theta)^2\,d\theta}{\int_0^{\pi/6} \frac{4}{3}\sin^2\theta\,d\theta} = \frac{2\pi}{2\pi - 3\sqrt{3}} \approx 5.780124 \neq \frac{52}{9}.\]
theorem conjecture_4 :
¬ Filter.atTop.Tendsto
(fun N : ℕ =>
(∑ p ∈ (Finset.range N).filter (fun p => p.Prime ∧ p % 3 = 1), ((xp p : ℝ) ^ 2)) /
(∑ p ∈ (Finset.range N).filter (fun p => p.Prime ∧ p % 3 = 1), ((yp p : ℝ) ^ 2)))
(nhds (52 / 9 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218585.lean, line 119.
Sources
TheoremPartitions \(2n + 1 = x + y\) with \(x^4 + y^4\) prime#
For \(n \ge 1\), \(a(n)\) is the number of ways to write \(2n + 1\) as \(x + y\) with \(0 < x < y\) such that \(x^4 + y^4\) is prime.
References: - A218656
Quoted from FormalConjectures/OEIS/218656.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 4 open. It also has 5 test statements, counted here but not shown.
OeisA218656.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n \ge 1\).
theorem conjecture_1 (n : ℕ) (hn : 1 ≤ n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218656.lean, line 113.
OeisA218656.conjecture_2
Open: stated without proof.
Conjecture: If \(x^4 + y^4\) in the definition of \(a(n)\) is replaced by \(x^2 + y^2\), then the count is positive for all \(n \ge 1\). - Thomas Ordowski, Nov 03 2012
theorem conjecture_2 (n : ℕ) (hn : 1 ≤ n) :
∃ x : ℕ, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime (x ^ 2 + (2 * n + 1 - x) ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218656.lean, line 122.
OeisA218656.conjecture_3
Open: stated without proof.
Conjecture: If \(x^4 + y^4\) in the definition of \(a(n)\) is replaced by \(x^8 + y^8\), then the count is positive for all \(n \ge 1\) except for \(2n + 1 \in \{7, 9, 55, 73, 75, 105\}\) (i.e., \(n \in \{3, 4, 27, 36, 37, 52\}\)). - Thomas Ordowski, Nov 03 2012; exceptions noted by Mauro Fiorentini, Sep 22 2023
theorem conjecture_3 (n : ℕ) (hn : 1 ≤ n) (h_exc : n ∉ ({3, 4, 27, 36, 37, 52} : Set ℕ)) :
∃ x : ℕ, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime (x ^ 8 + (2 * n + 1 - x) ^ 8)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218656.lean, line 133.
OeisA218656.conjecture_4
Open: stated without proof.
Conjecture: If \(x^4 + y^4\) in the definition of \(a(n)\) is replaced by \(x^{16} + y^{16}\), then the count is positive for all \(n \ge 1\) except for \(2n + 1 \in \{5, 9\}\) (i.e., \(n \in \{2, 4\}\)). - Thomas Ordowski, Nov 03 2012; exceptions noted by Mauro Fiorentini, Sep 22 2023
theorem conjecture_4 (n : ℕ) (hn : 1 ≤ n) (h_exc : n ∉ ({2, 4} : Set ℕ)) :
∃ x : ℕ, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime (x ^ 16 + (2 * n + 1 - x) ^ 16)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/218656.lean, line 143.
Sources
TheoremPrimes \(p < n\) with \(n^2 - n + p\) and \(n^2 + n - p\) prime#
For \(n \ge 1\), \(a(n)\) is the number of primes \(p < n\) such that \(n^2 - n + p\) and \(n^2 + n - p\) are both prime.
References: - A219023
Quoted from FormalConjectures/OEIS/219023.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 4 open. It also has 5 test statements, counted here but not shown.
OeisA219023.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 2732\).
theorem conjecture_1 (n : ℕ) (hn : 2732 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219023.lean, line 59.
OeisA219023.conjecture_2
Open: stated without proof.
Conjecture: For \(n > 3512\), there is a prime \(p \in (n, 2n)\) such that both \(n^2 - n + p\) and \(n^2 + n - p\) are prime. - Zhi-Wei Sun
theorem conjecture_2 (n : ℕ) (hn : 3512 < n) :
∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧
Nat.Prime (n ^ 2 - n + p) ∧ Nat.Prime (n ^ 2 + n - p)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219023.lean, line 68.
OeisA219023.conjecture_3
Open: stated without proof.
Conjecture: For \(n > 1828\), there is a prime \(p < n\) such that both \(n^2 - n - p\) and \(n^2 + n + p\) are prime. - Zhi-Wei Sun
theorem conjecture_3 (n : ℕ) (hn : 1828 < n) :
∃ p : ℕ, p.Prime ∧ p < n ∧
Nat.Prime (n ^ 2 - n - p) ∧ Nat.Prime (n ^ 2 + n + p)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219023.lean, line 79.
OeisA219023.conjecture_4
Open: stated without proof.
Conjecture: For \(n > 4517\), there is a prime \(p \in (n, 2n)\) such that both \(n^2 - n - p\) and \(n^2 + n + p\) are prime. - Zhi-Wei Sun
theorem conjecture_4 (n : ℕ) (hn : 4517 < n) :
∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧
Nat.Prime (n ^ 2 - n - p) ∧ Nat.Prime (n ^ 2 + n + p)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219023.lean, line 90.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.