Recurrence with fourth powers… to Number of primes of the form…
TheoremRecurrence with fourth powers of binomial coefficients#
The sequence is defined by \(a(1) = 2\), and for \(n \ge 2\),
\[(2n+1)^3 a(n) = 32n^3 a(n-1) + (21n^3 + 22n^2 + 8n + 1) \binom{2n-1}{n}^4.\]References: - A176477 - Z.-W. Sun, "Open Conjectures on Congruences", arXiv preprint arXiv:0911.5665 [math.NT], 2009-2011. - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.
Quoted from FormalConjectures/OEIS/176477.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 2 test statements, counted here but not shown.
OeisA176477.conjecture1
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/fd09021e79869476ef83cda231312f1a2a89c8d7/runs/oeis-open-lite-gpt6astra-37ly1phzfwj2ech4/oeis_a176477_conjecture/Submission/Spec.lean#L58383.
Each term \(a(n)\) is a positive integer. - Zhi-Wei Sun, Apr 06 2010
Proved in the OEIS Open project, see T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941.
theorem conjecture1 (n : ℕ) (hn : 1 ≤ n) : (a n).den = 1 ∧ 0 < a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/176477.lean, line 68.
OeisA176477.conjecture2
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/fd09021e79869476ef83cda231312f1a2a89c8d7/runs/oeis-open-lite-gpt6astra-37ly1phzfwj2ech4/oeis_a176477_conjecture/Submission/Spec.lean#L58383.
\(a(n)\) is odd if and only if \(n = 2, 2^2, 2^3, \dots\). - Zhi-Wei Sun, Apr 06 2010
Proved in the OEIS Open project, see T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941.
theorem conjecture2 (n : ℕ) (hn : 1 ≤ n) :
((a n).den = 1 ∧ Odd (a n).num) ↔ ∃ m : ℕ, 1 ≤ m ∧ n = 2 ^ m
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/176477.lean, line 81.
Sources
TheoremCentral binomial sum \(a(n) = \sum_{k=0}^n (-4)^k \binom{n}{k}^2 \binom{n-k}{k}^2\)#
The sequence is defined by
\[a(n) = \sum_{k=0}^n (-4)^k \binom{n}{k}^2 \binom{n-k}{k}^2.\]References: - A179524 - Z.-W. Sun, "Open Conjectures on Congruences", arXiv preprint arXiv:0911.5665 [math.NT], 2009-2011.
Quoted from FormalConjectures/OEIS/179524.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 5 open. It also has 5 test statements, counted here but not shown.
OeisA179524.conjecture1
Open: stated without proof.
If \(p\) is a prime with \(p \equiv 1, 9 \pmod{20}\) and \(p = x^2 + 5y^2\) with \(x, y\) integers, then \(\sum_{k=0}^{p-1} a(k) \equiv 4x^2 - 2p \pmod{p^2}\). - Zhi-Wei Sun, Jul 01 2010
theorem conjecture1 (p : ℕ) (hp : p.Prime)
(h_mod : (p : ℤ) ≡ 1 [ZMOD 20] ∨ (p : ℤ) ≡ 9 [ZMOD 20])
(x y : ℤ) (h_sq : (p : ℤ) = x ^ 2 + 5 * y ^ 2) :
∑ k ∈ Finset.range p, a k ≡ 4 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179524.lean, line 60.
OeisA179524.conjecture2
Open: stated without proof.
If \(p\) is a prime with \(p \equiv 3, 7 \pmod{20}\) and \(2p = x^2 + 5y^2\) with \(x, y\) integers, then \(\sum_{k=0}^{p-1} a(k) \equiv 2x^2 - 2p \pmod{p^2}\). - Zhi-Wei Sun, Jul 01 2010
theorem conjecture2 (p : ℕ) (hp : p.Prime)
(h_mod : (p : ℤ) ≡ 3 [ZMOD 20] ∨ (p : ℤ) ≡ 7 [ZMOD 20])
(x y : ℤ) (h_sq : 2 * (p : ℤ) = x ^ 2 + 5 * y ^ 2) :
∑ k ∈ Finset.range p, a k ≡ 2 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179524.lean, line 72.
OeisA179524.conjecture3
Open: stated without proof.
If \(p\) is a prime with \(p \equiv 11, 13, 17, 19 \pmod{20}\), then \(\sum_{k=0}^{p-1} a(k) \equiv 0 \pmod{p^2}\). - Zhi-Wei Sun, Jul 01 2010
theorem conjecture3 (p : ℕ) (hp : p.Prime)
(h_mod : (p : ℤ) ≡ 11 [ZMOD 20] ∨ (p : ℤ) ≡ 13 [ZMOD 20] ∨
(p : ℤ) ≡ 17 [ZMOD 20] ∨ (p : ℤ) ≡ 19 [ZMOD 20]) :
∑ k ∈ Finset.range p, a k ≡ 0 [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179524.lean, line 84.
OeisA179524.conjecture4
Open: stated without proof.
\(\sum_{k=0}^{n-1}(20k+17)a(k) \equiv 0 \pmod n\) for all \(n=1,2,3,\dots\). - Zhi-Wei Sun, Jul 01 2010
theorem conjecture4 (n : ℕ) (hn : 1 ≤ n) :
(n : ℤ) ∣ ∑ k ∈ Finset.range n, ((20 * (k : ℤ) + 17) * a k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179524.lean, line 95.
OeisA179524.conjecture5
Open: stated without proof.
\(\sum_{k=0}^{p-1}(20k+17)a(k) \equiv p(10(-1/p)+7) \pmod{p^2}\) for any odd prime \(p\). - Zhi-Wei Sun, Jul 01 2010
theorem conjecture5 (p : ℕ) [hp : Fact p.Prime] (_hp2 : p ≠ 2) :
(∑ k ∈ Finset.range p, ((20 * (k : ℤ) + 17) * a k)) ≡
(p : ℤ) * (10 * legendreSym p (-1) + 7) [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179524.lean, line 104.
Sources
TheoremCentral binomial sum \(a(n) = \sum_{k=0}^n \binom{n}{k}^2 \binom{n-k}{k}^2 (-16)^k\)#
The sequence is defined by
\[a(n) = \sum_{k=0}^n \binom{n}{k}^2 \binom{n-k}{k}^2 (-16)^k.\]References: - A179537 - Z.-W. Sun, "Open Conjectures on Congruences", arXiv preprint arXiv:0911.5665 [math.NT], 2009-2011.
Quoted from FormalConjectures/OEIS/179537.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.
OeisA179537.conjecture1
Open: stated without proof.
If \(p\) is a prime with \((p/7) = 1\) and \(p = x^2 + 7y^2\) with \(x, y\) integers, then \(\sum_{k=0}^{p-1} (-1)^k a(k) \equiv 4x^2 - 2p \pmod{p^2}\). - Zhi-Wei Sun, Jul 17 2010
theorem conjecture1 (p : ℕ) [Fact p.Prime] (hp7 : p ≠ 7)
(h_leg : letI : Fact (Nat.Prime 7) := ⟨by decide⟩; legendreSym 7 p = 1)
(x y : ℤ) (h_sq : (p : ℤ) = x ^ 2 + 7 * y ^ 2) :
(∑ k ∈ Finset.range p, (-1 : ℤ) ^ k * a k) ≡
4 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179537.lean, line 65.
OeisA179537.conjecture2
Open: stated without proof.
If \(p\) is a prime with \((p/7) = -1\), then \(\sum_{k=0}^{p-1} (-1)^k a(k) \equiv 0 \pmod{p^2}\). - Zhi-Wei Sun, Jul 17 2010
theorem conjecture2 (p : ℕ) [Fact p.Prime] (hp7 : p ≠ 7)
(h_leg : letI : Fact (Nat.Prime 7) := ⟨by decide⟩; legendreSym 7 p = -1) :
(∑ k ∈ Finset.range p, (-1 : ℤ) ^ k * a k) ≡ 0 [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179537.lean, line 78.
OeisA179537.conjecture3
Open: stated without proof.
\(\sum_{k=0}^{n-1} (42k + 37) (-1)^k a(k) \equiv 0 \pmod n\) for all \(n \ge 1\). - Zhi-Wei Sun, Jul 17 2010
theorem conjecture3 (n : ℕ) (hn : 1 ≤ n) :
(n : ℤ) ∣ ∑ k ∈ Finset.range n, ((42 * (k : ℤ) + 37) * (-1 : ℤ) ^ k * a k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179537.lean, line 88.
OeisA179537.conjecture4
Open: stated without proof.
\(\sum_{k=0}^{p-1} (42k + 37) (-1)^k a(k) \equiv p(21(p/7) + 16) \pmod{p^2}\) for any prime \(p \ne 7\). - Zhi-Wei Sun, Jul 17 2010
theorem conjecture4 (p : ℕ) [Fact p.Prime] (_hp7 : p ≠ 7) :
letI : Fact (Nat.Prime 7) := ⟨by decide⟩
(∑ k ∈ Finset.range p, ((42 * (k : ℤ) + 37) * (-1 : ℤ) ^ k * a k)) ≡
(p : ℤ) * (21 * legendreSym 7 p + 16) [ZMOD (p : ℤ) ^ 2]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/179537.lean, line 97.
Sources
TheoremDifference of digit sums in base 3 and base 2#
Difference of sums of digits of \(n\) in ternary and in binary:
\[a(n) = \sum \mathrm{digits}_3(n) - \sum \mathrm{digits}_2(n).\]References: - A180017
Quoted from FormalConjectures/OEIS/180017.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.
OeisA180017.conjecture
Open: stated without proof.
"This sequence is positive on average, since 1/log(3) > 1/log(4). Do all integers appear infinitely often?" - Charles R Greathouse IV, Feb 07 2013
theorem conjecture (z : ℤ) : Set.Infinite {n : ℕ | a n = z}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/180017.lean, line 56.
Sources
TheoremVan Eck's sequence (OEIS A181391)#
Van Eck's sequence starts with zero. If the current value has occurred before, the next value is the distance to its most recent earlier occurrence; otherwise the next value is zero.
References: - OEIS A181391 - N. J. A. Sloane, Some Open Problems
Quoted from FormalConjectures/OEIS/181391.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 and 1 API statement, counted here but not shown.
OeisA181391.conjecture
Open: stated without proof.
OEIS A181391 conjectures: "every number eventually appears."
theorem conjecture : Function.Surjective a
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/181391.lean, line 109.
Sources
TheoremSum of fourth powers of Fibonacci-like binomial coefficients#
The sequence is defined by
\[a(n) = \sum_{k=0}^{\lfloor n/2 \rfloor} \binom{n-k}{k}^4.\]References: - A181546
Quoted from FormalConjectures/OEIS/181546.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.
OeisA181546.conjecture
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-full-50usd-ant-j0j0g4uzligm1k41/oeis_181546_conjecture_0/Submission/Spec.lean#L1210.
Conjecture: Given \(F(n,L) = \sum_{k=0}^{\lfloor n/2 \rfloor} \binom{n-k}{k}^L\), then \(\lim_{n\to\infty} F(n+1,L)/F(n,L) = (\mathrm{Fibonacci}(L)\sqrt{5} + \mathrm{Lucas}(L))/2\) for \(L \ge 0\) where \(\mathrm{Fibonacci}(n) = \mathrm{A000045}(n)\) and \(\mathrm{Lucas}(n) = \mathrm{A000032}(n)\).
theorem conjecture (L : ℕ) :
Tendsto (fun n => (F (n + 1) L : ℝ) / (F n L : ℝ)) atTop (nhds (limitValue L))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/181546.lean, line 80.
Sources
TheoremProduct of two consecutive primes modulo the next prime#
The sequence is defined by
\[a(n) = \mathrm{prime}(n) \cdot \mathrm{prime}(n+1) \bmod \mathrm{prime}(n+2),\]where \(\mathrm{prime}(k)\) is the \(k\)-th prime number (\(\mathrm{prime}(1)=2\)).
References: - A182126
Quoted from FormalConjectures/OEIS/182126.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 4 test statements, counted here but not shown.
OeisA182126.conjecture1
Open: stated without proof.
Conjecture: For \(x > 10^9\), the most frequent value in \(a(n)\), \(n=1\dots x\), has form \(120k\).
theorem conjecture1 (x : ℕ) (hx : 10 ^ 9 < x) (v₀ : ℕ) (hv : IsMostFrequent x v₀) :
120 ∣ v₀
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/182126.lean, line 86.
OeisA182126.conjecture2
Open: stated without proof.
Let \(b = \mathrm{prime}(n+2) - \mathrm{prime}(n)\) and \(c = \mathrm{prime}(n+2) - \mathrm{prime}(n+1)\). Conjecture: for \(n > 61\), \(a(n) = b \cdot c\). - Charles R Greathouse IV, May 11 2012
theorem conjecture2 (n : ℕ) (hn : 61 < n) :
let b := prime (n + 2) - prime n
let c := prime (n + 2) - prime (n + 1)
a n = b * c
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/182126.lean, line 96.
OeisA182126.conjecture3
Open: stated without proof.
Are 2, 7, 11, 13, 29 the only primes in this sequence? - Hugo Pfoertner, Sep 22 2025
theorem conjecture3 (n : ℕ) (hn : 0 < n) :
(a n).Prime ↔ a n ∈ ([2, 7, 11, 13, 29] : List ℕ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/182126.lean, line 107.
Sources
TheoremRecurrence with bitwise XOR#
The sequence is defined by \(a(0) = 0\), \(a(1) = 1\), and for \(n \ge 0\),
\[a(n+2) = (a(n+1) \mathbin{\mathrm{XOR}} (n+2)) - a(n),\]where \(\mathrm{XOR}\) is the bitwise exclusive-or operator on integers.
References: - A182510
Quoted from FormalConjectures/OEIS/182510.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 7 test statements, counted here but not shown.
OeisA182510.conjecture1
Open: stated without proof.
Conjecture: the sequence contains 8 zeros.
theorem conjecture1 : Set.ncard {n : ℕ | a n = 0} = 8
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/182510.lean, line 64.
OeisA182510.conjecture2
Open: stated without proof.
Conjecture: more positive terms than negative.
As \(n \to \infty\), the count of positive terms is greater than the count of negative terms.
The requirement that \(n\) is large enough is needed, since the claim fails for \(n = 100\).
theorem conjecture2 :
∀ᶠ n in Filter.atTop,
((Finset.range n).filter (fun k => a k < 0)).card <
((Finset.range n).filter (fun k => 0 < a k)).card
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/182510.lean, line 75.
Sources
TheoremNumber of odd primes between \(n^2\) and \((n+1)^2\) with \((n/p) = 1\)#
\(a(n)\) is the number of odd primes \(p\) between \(n^2\) and \((n+1)^2\) such that the Legendre symbol \(\left(\frac{n}{p}\right) = 1\).
References: - A185150 - Z.-W. Sun, "Conjectures involving primes and quadratic forms", arXiv preprint arXiv:1211.1588 [math.NT], 2012.
Quoted from FormalConjectures/OEIS/185150.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.
OeisA185150.conjecture
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 0\). - Zhi-Wei Sun, Dec 29 2012
theorem conjecture (n : ℕ) (hn : 0 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/185150.lean, line 74.
Sources
TheoremCoefficients of \(\prod_{k>0} (1 - x^k/k!)\)#
The sequence \(a(n)\) has exponential generating function
\[E(x) = \prod_{k=1}^\infty \left(1 - \frac{x^k}{k!}\right),\]so that \(a(n) = n! [x^n] \prod_{k=1}^n \left(1 - \frac{x^k}{k!}\right)\).
Since \(a(n)\) is a sum of multinomial coefficients with \(\pm\) signs, it is always an integer.
References: - A185895
Quoted from FormalConjectures/OEIS/185895.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 solved. It also has 5 test statements, counted here but not shown.
OeisA185895.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-lite-200usd-sol-nk5wh4g0vh3546nm/oeis_185895_conjecture_1/Submission/Spec.lean#L4835.
\(a(n)\) differs in sign from \(a(n-1)\) if and only if \(n\) is a triangular number (checked up to \(n = 1225 = (50 \cdot 51)/2\)). - Peter Bala, Mar 17 2022
theorem conjecture_1 (n : ℕ) (hn : 0 < n) :
a n * a (n - 1) < 0 ↔ n.IsTriangular
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/185895.lean, line 105.
OeisA185895.conjecture_2
Solved: stated here; a Lean proof is at https://github.com/kei825/oeis-a185895-conjecture2/blob/8ddd5a7d2bde415940f944440921fd760283f79d/OeisA185895Conjecture2.lean#L4959-L4961.
The coefficients \(c(n)\) of \(A(x)^2 = (\sum_{n \ge 0} a(n) x^n)^2\) differ in sign from \(c(n-1)\) if and only if \(n\) is a triangular number. - Peter Bala, Mar 17 2022
Proof sketch (the kernel-checked development lives at the
formal_proofpermalink below). Write \(a(n)/n! = \sum_j (-1)^j L_j(n)\), where \(L_j(n)\) is the sum of \(\prod_{s \in S} 1/s!\) over all sets \(S\) of \(j\) distinct positive integers with sum \(n\). A "down map" (lowering by one the least element of \(S\) above its first gap) gives \(L_{k-1}(n) \le \frac{91}{100} L_k(n)\) for all \(k \ge 1\) and \(n \ge k(k+1)/2\). Hence the top nonzero layer \(L_m(n)\) dominates, where \(m(m+1)/2 \le n < (m+1)(m+2)/2\); this reprovesconjecture_1and gives \(|a(n)| \ge \frac{9}{100} n! L_m(n)\). Since \(c(n) = 2a(n) + \sum_{0\lt k\lt n} a(k)a(n-k)\), the sign of \(c(n)\) equals that of \(a(n)\) whenever \(\sum_{0\lt k\lt n} |a(k)a(n-k)| < 2|a(n)|\). For \(n \le 2500\), conjecture 2 is checked in the kernel from a certified table of \(a(n)\); for \(n > 2500\), explicit estimates (rational arithmetic and elementary bounds only) bound the cross sum by \(0.18 \cdot n! L_m(n)\), which is less than \(2|a(n)|\).
theorem conjecture_2 (n : ℕ) (hn : 0 < n) :
c n * c (n - 1) < 0 ↔ n.IsTriangular
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/185895.lean, line 130.
OeisA185895.conjecture_3
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a185895-conjecture3/blob/e40e3db2b47beeef22b00a481fc3a41b518168d9/lean/OeisA185895Conjecture3FC.lean#L579-L589.
The Gauss congruences \(a(n \cdot p^k) \equiv a(n \cdot p^{k-1}) \pmod{p^k}\) hold for all primes \(p\) and positive integers \(n\) and \(k\). - Peter Bala, Mar 17 2022
theorem conjecture_3 (p : ℕ) (hp : p.Prime) (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
a (n * p ^ k) ≡ a (n * p ^ (k - 1)) [ZMOD (p : ℤ) ^ k]
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/185895.lean, line 143.
Sources
TheoremNumber of ways to write \(n = x + y\) (\(0 < x < y < n\)) with \(6x \pm 1\) and \(6y \pm 1\) prime#
The sequence \(a(n)\) counts the number of ways to write \(n = x + y\) with \(0 < x < y < n\) such that \(6x - 1\), \(6x + 1\), \(6y - 1\), and \(6y + 1\) are all prime numbers.
References: - A187759 - Conjectures involving primes and quadratic forms by Zhi-Wei Sun, arXiv:1211.1588 (2012)
Quoted from FormalConjectures/OEIS/187759.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.
OeisA187759.conjecture
Open: stated without proof.
Conjecture: If \(n > 200\) is not among \(211, 226, 541, 701\), then \(a(n) > 0\). - Zhi-Wei Sun, Jan 03 2013
theorem conjecture (n : ℕ) (hn : 200 < n) (hnot : n ∉ ({211, 226, 541, 701} : Finset ℕ)) :
0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/187759.lean, line 70.
Sources
TheoremNormalized convolution of \(\binom{6k}{3k}\binom{3k}{k}\)#
The sequence \(a(n)\) is defined by
\[a(n) = \frac{\sum_{k=0}^n \binom{6k}{3k}\binom{3k}{k} \binom{6(n-k)}{3(n-k)}\binom{3(n-k)}{n-k}}{(2n-1)\binom{3n}{n}}.\]References: - A189286 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.
Quoted from FormalConjectures/OEIS/189286.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 1 open, 1 solved and 1 textbook result. It also has 5 test statements, counted here but not shown.
OeisA189286.conjecture_1
Solved: stated here without proof.
Conjecture: \(a(n)\) is an integer for every \(n = 0, 1, 2, \dots\). - Zhi-Wei Sun, Apr 19 2011
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 : ℕ) : (a n).den = 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/189286.lean, line 72.
OeisA189286.conjecture_2
Textbook result, stated without proof.
Conjecture (i): \(a(n)^{1/n}\) tends to \(64\) as \(n\) tends to infinity. - Zhi-Wei Sun, Apr 19 2011
theorem conjecture_2 :
Filter.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (n : ℝ))) Filter.atTop (nhds 64)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/189286.lean, line 80.
OeisA189286.conjecture_3
Open: stated without proof.
Conjecture (ii): For any positive integer \(n\), we have \(a(n) \equiv 0 \pmod 8\), and \(a(n)/8\) is odd if and only if \(n\) is a power of two. - Zhi-Wei Sun, Apr 19 2011
theorem conjecture_3 (n : ℕ) (hn : 0 < n) :
∃ m : ℤ, a n = 8 * m ∧ (Odd m ↔ ∃ k : ℕ, n = 2 ^ k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/189286.lean, line 90.
Sources
TheoremPrimorial squared plus one#
The sequence \(a(n)\) is defined by \(a(n) = (p_n\#)^2 + 1\), where \(p_n\# = \prod_{k=0}^{n-1} p_k\) is the \(n\)-th primorial (A002110).
References: - A189409
Quoted from FormalConjectures/OEIS/189409.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.
OeisA189409.conjecture_1
Open: stated without proof.
It is unknown whether or not numbers in this sequence are always squarefree. - John M. Campbell, Apr 21 2011
theorem conjecture_1 : ∀ n : ℕ, Squarefree (a n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/189409.lean, line 58.
OeisA189409.conjecture_2
Open: stated without proof.
It is unknown whether or not there exist infinitely many primes in this sequence. - John M. Campbell, Apr 21 2011
theorem conjecture_2 : Set.Infinite {n : ℕ | (a n).Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/189409.lean, line 66.
Sources
TheoremSequence \(a(n) = n + \lfloor n r / t \rfloor + \lfloor n s / t \rfloor\)#
The sequence \(a(n)\) is given by \(a(n) = n + \lfloor n r / t \rfloor + \lfloor n s / t \rfloor\) where \(r = 1\), \(s = \sqrt{5/4}\), and \(t = \sqrt{4/5}\). Equivalently,
\[a(n) = 2n + \lfloor n \sqrt{5/4} \rfloor + \lfloor n/4 \rfloor.\]References: - A190363
Quoted from FormalConjectures/OEIS/190363.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.
OeisA190363.conjecture
Solved: stated here without proof.
Conjecture: \(a(n)\) satisfies the linear recurrence with constant coefficients \(0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, -1\), i.e., \(a(n + 21) = a(n + 17) + a(n + 4) - a(n)\) for \(n \ge 1\). - Harvey P. Dale, Jan 28 2025
The conjecture is false: the recurrence first fails at \(n = 140\), i.e. for the term \(a(140 + 21) = a(161) = 543 \ne 542 = a(157) + a(144) - a(140)\).
Since \(\lim_{n\to\infty} \frac{a(n)}{n} = \frac{9}{4} + \frac{\sqrt{5}}{2}\) is irrational, no linear recurrence with constant integer coefficients can hold. Indeed, it follows from known results that if \(a(n)\) satisfies a linear recurrence with constant integer coefficients and \(\lim_{n \to \infty} \frac{a_n}{n} = \alpha\) exists, then \(\alpha\) must be rational.
theorem conjecture :
¬ ∀ n : ℕ, 1 ≤ n → (a (n + 21) : ℤ) = a (n + 17) + a (n + 4) - a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/190363.lean, line 110.
Sources
TheoremLinear recurrence \(a(n) = 5a(n-1) - 8a(n-2)\) with \(a(0)=0, a(1)=1\)#
The sequence \(a(n)\) satisfies the linear recurrence relation \(a(n) = 5a(n-1) - 8a(n-2)\) with initial values \(a(0) = 0\) and \(a(1) = 1\).
References: - A190969 - Conjectures involving primes and quadratic forms by Zhi-Wei Sun, arXiv:1211.1588 (2012)
Quoted from FormalConjectures/OEIS/190969.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.
OeisA190969.conjecture_1
Open: stated without proof.
Conjecture: Let \(S(p) := \sum_{k=0}^{p-1} a(4k) \binom{2k}{k}^3 / (-4096)^k\). Then \(S(p) \equiv 0 \pmod{p^2}\) for every odd prime \(p\). - Zhi-Wei Sun, Mar 13 2013
theorem conjecture_1 (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :
sMod p 2 = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/190969.lean, line 74.
OeisA190969.conjecture_2
Open: stated without proof.
Conjecture: Let \(S(p) := \sum_{k=0}^{p-1} a(4k) \binom{2k}{k}^3 / (-4096)^k\). Then \(S(p) \equiv 0 \pmod{p^3}\) for any odd prime \(p \equiv 1, 2, 4 \pmod 7\). - Zhi-Wei Sun, Mar 13 2013
theorem conjecture_2 (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2)
(h7 : p % 7 ∈ ({1, 2, 4} : Finset ℕ)) :
sMod p 3 = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/190969.lean, line 84.
Sources
TheoremRepresentations of \(n = p + q + (n \bmod 2)q\) with Jacobi symbol constraints#
The sequence \(a(n)\) counts the number of ways to write \(n = p + q + (n \bmod 2)q\), where \(p\) is an odd prime and \(q \le n/2\) is a prime such that \(\left(\frac{q}{n}\right) = 1\) if \(n\) is odd, and \(\left(\frac{(q+1)/2}{n+1}\right) = 1\) if \(n\) is even.
References: - A191004 - Conjectures involving primes and quadratic forms by Zhi-Wei Sun, arXiv:1211.1588 (2012)
Quoted from FormalConjectures/OEIS/191004.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 7 test statements, counted here but not shown.
OeisA191004.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 5\). - Zhi-Wei Sun, Dec 30 2012
theorem conjecture_1 (n : ℕ) (hn : 5 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/191004.lean, line 80.
OeisA191004.conjecture_2
Open: stated without proof.
Refinement conjecture (odd case): Any odd number \(2n+1 > 64\) not among \(105, 247, 255, 1105\) can be written as \(p + 2q\), where \(p\) and \(q\) are primes, and \(\left(\frac{q}{p'}\right) = 1\) for any prime divisor \(p'\) of \(2n+1\). - Zhi-Wei Sun, Dec 30 2012
theorem conjecture_2 (m : ℕ) (hm : 64 < m) (hodd : Odd m)
(hnot : m ∉ ({105, 247, 255, 1105} : Finset ℕ)) :
∃ p q : ℕ, p.Prime ∧ q.Prime ∧ m = p + 2 * q ∧
∀ p' ∈ m.primeFactors, jacobiSym (q : ℤ) p' = 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/191004.lean, line 90.
OeisA191004.conjecture_3
Open: stated without proof.
Refinement conjecture (even case): Any even number \(m = 2n > 8\) not among \(32\) and \(152\) can be written as \(p + q\), where \(p\) and \(q \le m/2\) are primes, and \(\left(\frac{(q+1)/2}{p'}\right) = 1\) for any prime divisor \(p'\) of \(m+1\). (The OEIS comment writes \(q \le n/2\) after renaming the argument of \(a(\cdot)\) to \(2n\), which is a slip for \(q \le (2n)/2 = n = m/2\), matching the bound in the definition of \(a(2n)\) and yielding the stated exceptional set \(\{32, 152\}\).) - Zhi-Wei Sun, Dec 30 2012
theorem conjecture_3 (m : ℕ) (hm : 8 < m) (heven : Even m)
(hnot : m ∉ ({32, 152} : Finset ℕ)) :
∃ p q : ℕ, p.Prime ∧ q.Prime ∧ m = p + q ∧ q ≤ m / 2 ∧
∀ p' ∈ (m + 1).primeFactors, jacobiSym (((q + 1) / 2) : ℤ) p' = 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/191004.lean, line 106.
Sources
TheoremNumber of distinct sums of distinct proper divisors of \(n\)#
The sequence \(a(n)\) counts the number of distinct sums of non-empty subsets of the proper divisors of \(n\).
References: - A193279
Quoted from FormalConjectures/OEIS/193279.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 solved and 1 textbook result. It also has 6 test statements, counted here but not shown.
OeisA193279.a_eq_self_of_perfect_of_even
Textbook result, stated without proof.
If \(n\) is an even perfect number, then \(a(n) = n\). - Michael Engling, Jul 20 2011
theorem a_eq_self_of_perfect_of_even (n : ℕ) (hperf : n.Perfect) (heven : Even n) :
a n = n
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/193279.lean, line 63.
OeisA193279.conjecture
Solved: stated here without proof.
Is the converse true, i.e., if \(a(n) = n\), is \(n\) necessarily an even perfect number? - Michael Engling, Jul 20 2011
The answer is no: for example, \(n = 492 = 2^2 \cdot 3 \cdot 41\) and \(n = 1652 = 2^2 \cdot 7 \cdot 59\) satisfy \(a(n) = n\) but are abundant rather than perfect.
theorem conjecture : ¬ ∀ n : ℕ, 0 < n → a n = n → n.Perfect ∧ Even n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/193279.lean, line 75.
Sources
TheoremSize of smallest subset of \(\{1, 2, \dots, n\}\) with distinct subset sums#
Size of the smallest subset \(S\) of \(T = \{1,2,3,\dots,n\}\) such that \(S \cdot S\) contains \(T\), where \(S \cdot S\) is the set of all products of elements of \(S\).
References: - A194806 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/194806.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.
OeisA194806.a_div_prime_counting_bounded
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/194806.wip.lean#L472.
Is \(a(n) / \pi(n)\) bounded as \(n \to \infty\)? - Robert Israel, Jan 09 2017
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_div_prime_counting_bounded : ∃ C : ℝ,
∀ n : ℕ, 2 ≤ n → (a n : ℝ) / (Nat.primeCounting n : ℝ) ≤ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/194806.lean, line 115.
Sources
TheoremDenominator of \(B_{n+1}(x) - B_{n+1}\)#
The sequence \(a(n)\) is the least common multiple of the denominators of the coefficients of the polynomial \(B_{n+1}(x) - B_{n+1}\), where \(B_m(x) = \sum_{k=0}^m \binom{m}{k} B_{m-k} x^k\) is the \(m\)-th Bernoulli polynomial and \(B_m\) is the \(m\)-th Bernoulli number.
References: - A195441 - Finiteness of Bernoulli polynomials by Bernd C. Kellner, J. Integer Seq. 27 (2024)
Quoted from FormalConjectures/OEIS/195441.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.
OeisA195441.conjecture
Open: stated without proof.
The equation \(a(n-1) = \operatorname{rad}(n+1)\) has only finitely many solutions, where \(\operatorname{rad}(n)\) is the radical of \(n\). It is conjectured that \(S = \{3, 5, 8, 9, 11, 27, 29, 35, 59\}\) is the full set of all such solutions. - Bernd C. Kellner, Oct 18 2023
theorem conjecture :
{n : ℕ | 1 ≤ n ∧ a (n - 1) = UniqueFactorizationMonoid.radical (n + 1)} =
({3, 5, 8, 9, 11, 27, 29, 35, 59} : Finset ℕ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/195441.lean, line 68.
Sources
TheoremNumber of primes of the form \(2^n \pm 2^k \pm 1\) with \(0 \le k < n\)#
The sequence \(a(n)\) counts the number of distinct primes of the form \(2^n \pm 2^k \pm 1\) for \(0 \le k < n\).
References: - A196697
Quoted from FormalConjectures/OEIS/196697.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.
OeisA196697.conjecture_1
Open: stated without proof.
Conjecture: all terms of this sequence are greater than \(0\). - Lei Zhou, Oct 05 2011
theorem conjecture_1 (n : ℕ) (hn : 1 ≤ n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/196697.lean, line 63.
OeisA196697.conjecture_2
Open: stated without proof.
Conjecture: 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/196697.lean, line 71.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.