Representations of \(n\) using… to Partitions \(n = p + q\) with…
TheoremRepresentations of \(n\) using prime pairs with prime gaps of \(6\)#
Number of ways to write \(n = p + q(3 - (-1)^n)/2\) with \(p > q\) and \(p, q, p - 6, q + 6\) all prime.
References: - A219055
Quoted from FormalConjectures/OEIS/219055.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.
OeisA219055.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all even \(n > 8012\) and odd \(n > 15727\).
theorem conjecture_1 (n : ℕ) (hn : (Even n ∧ 8012 < n) ∨ (Odd n ∧ 15727 < n)) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219055.lean, line 63.
OeisA219055.conjecture_2
Open: stated without proof.
Conjecture: For any two multiples \(d_1\) and \(d_2\) of \(6\), all sufficiently large integers \(n\) can be written as \(p + q(3 - (-1)^n)/2\) with \(p > q\) and \(p, q, p - d_1, q + d_2\) all prime. - Zhi-Wei Sun
theorem conjecture_2 (d₁ d₂ : ℤ) (hd₁ : 6 ∣ d₁) (hd₂ : 6 ∣ d₂) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ p q p' q' : ℕ, q < p ∧ p.Prime ∧ q.Prime ∧ p'.Prime ∧ q'.Prime ∧
(p : ℤ) - d₁ = p' ∧ (q : ℤ) + d₂ = q' ∧ n = p + (1 + n % 2) * q
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219055.lean, line 73.
Sources
TheoremPartitions of \(n\) into \(x + y\) with \((xy)^2 + 1\) prime#
Number of ways to write \(n = x + y\) (\(0 < x \le y\)) with \((xy)^2 + 1\) prime.
References: - A219791
Quoted from FormalConjectures/OEIS/219791.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.
OeisA219791.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) if \(n\) is different from \(1, 6, 16, 24\).
theorem conjecture_1 (n : ℕ) (hn : n > 0) (h1 : n ≠ 1) (h6 : n ≠ 6) (h16 : n ≠ 16) (h24 : n ≠ 24) :
a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219791.lean, line 56.
OeisA219791.conjecture_2
Open: stated without proof.
Conjecture: For any positive integer \(k\), each sufficiently large integer \(n\) can be written as \(x + y\) (\(x > 0, y > 0\)) with \((xy)^{2^k} + 1\) prime. - Zhi-Wei Sun
theorem conjecture_2 (k : ℕ) (hk : 0 < k) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧ Nat.Prime ((x * y) ^ (2 ^ k) + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219791.lean, line 67.
Sources
TheoremPartitions of \(n\) into \(x + y\) with \((xy)^2 + xy + 1\) prime#
Number of ways to write \(n\) as \(x + y\) with \(0 < x \le y\) and \((xy)^2 + xy + 1\) prime.
References: - A219838
Quoted from FormalConjectures/OEIS/219838.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 6 test statements, counted here but not shown.
OeisA219838.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture_1 (n : ℕ) (hn : n > 1) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219838.lean, line 62.
OeisA219838.conjecture_2
Open: stated without proof.
The author also guesses that any integer \(n > 1157\) can be written as \(x + y\) with \(x\) and \(y\) positive integers, and \((xy)^2 + xy + 1\) and \((xy)^2 + xy - 1\) twin primes.
theorem conjecture_2 (n : ℕ) (hn : n > 1157) :
∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime ((x * y) ^ 2 + x * y - 1) ∧ Nat.Prime ((x * y) ^ 2 + x * y + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219838.lean, line 70.
OeisA219838.conjecture_3
Open: stated without proof.
Conjecture: For each prime \(p\), any sufficiently large integer \(n\) can be written as \(x + y\), where \(x\) and \(y\) are positive integers with \(\frac{(xy)^p - 1}{xy - 1}\) prime. - Zhi-Wei Sun
theorem conjecture_3 (p : ℕ) (hp : p.Prime) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime (((x * y) ^ p - 1) / (x * y - 1))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/219838.lean, line 82.
Sources
TheoremA double sum of five binomial factors#
The sequence is defined by \(a(n)=\sum_{j,k=0}^{n}\binom{n}{j}^2\binom{n}{k}^2\binom{n+j}{n}\binom{n+k}{n}\binom{j+k}{n}\).
References: - A220119 - [Li26] Wentao Li, A proof of the OEIS A220119 conjecture, 2026.
Quoted from FormalConjectures/OEIS/220119.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.
OeisA220119.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewProofs/A220119.lean#L1702.
Conjecture 1: "Conjecture: For \(n > 0\), \(a(n)\) is always divisible by \((n+1) * (n+2)\)." - F. Chapoton, Apr 23 2026.
The restriction \(n > 0\) is necessary since \(a(0) = 1\). Proved and formalized in Lean by Wentao Li, with AI assistance; see [Li26].
theorem conjecture_1 (n : ℕ) (hn : 0 < n) : (n + 1) * (n + 2) ∣ a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/220119.lean, line 67.
Sources
TheoremTrajectory of \(64\) under the map \(n \to \text{A006368}(n)\)#
The map is given by
\[f(n) = \begin{cases} 3n/2 & \text{if } n \equiv 0 \pmod 2, \\ (3n+1)/4 & \text{if } n \equiv 1 \pmod 4, \\ (3n-1)/4 & \text{if } n \equiv 3 \pmod 4. \end{cases}\]References: - A223086
Quoted from FormalConjectures/OEIS/223086.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 7 test statements, counted here but not shown.
OeisA223086.conjecture
Open: stated without proof.
It is conjectured that this trajectory does not close on itself.
theorem conjecture (i j : ℕ) (hi : 0 < i) (hj : 0 < j) (h : a i = a j) : i = j
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/223086.lean, line 77.
Sources
TheoremExistence of integers \(k\) with \(k^2 \operatorname{XOR} (k+1)^2 = (2n+1)^2\)#
a: \(a(n) = \text{least } k \text{ such that } \sqrt{k^2 \operatorname{XOR} (k+1)^2} = 2n+1\), \(a(n) = -1 \text{ if there is no such } k\). This is equivalent to finding the smallest \(k \in \mathbb{N}\) such that \(k^2 \oplus (k+1)^2 = (2n+1)^2\). We use the set infimum (\(\operatorname{sInf}\)) to denote the least element of the set of natural numbers satisfying the condition. Since Mathlib's
sInfon a subset ofℕgives a result inℕ, this definition is only completely faithful to the OEIS when the set is non-empty. The OEIS definition implies that the set of k's is non-empty for all n.References: - A224515 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/224515.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements and 1 API statement, counted here but not shown.
OeisA224515.exists_xor_sq_eq
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/224515.wip.lean#L268.
Conjecture: \(a(n) \ge 0\), i.e., for every \(n\) there exists \(k\) such that \(\sqrt{k^2 \oplus (k+1)^2} = 2n+1\).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem exists_xor_sq_eq (n : ℕ) : ∃ k : ℕ, Nat.xor (k ^ 2) ((k + 1) ^ 2) = (2 * n + 1) ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/224515.lean, line 111.
Sources
TheoremDeterminant of Legendre symbol matrix with factorial shifts#
Determinant of the \((p_n-1)/2\)-by-\((p_n-1)/2\) matrix with \((i,j)\)-entry being the Legendre symbol
\[\left(\frac{i^2 - \left(\frac{p_n-1}{2}\right)! j}{p_n}\right),\]where \(p_n\) is the \(n\)-th prime (\(n \ge 2\)).
References: - A226163 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.
Quoted from FormalConjectures/OEIS/226163.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.
OeisA226163.conjecture
Solved: stated here without proof.
Conjecture: \(a(n) = 0\) if and only if \(p_n \equiv 3 \pmod 4\). - Zhi-Wei Sun, Aug 13 2013
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 (n : ℕ) (hn : 2 ≤ n) :
a n = 0 ↔ Nat.nth Nat.Prime (n - 1) % 4 = 3
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/226163.lean, line 114.
Sources
TheoremRepresentation of sequence terms by harmonic numbers \(\lfloor \frac{1}{2H(n) - H(n^2+n-1) - \gamma} \rfloor\)#
A227582: Expansion of \((2+3x+2x^2+2x^3+3x^4+x^5-x^6)/(1-2x+x^2-x^5+2x^6-x^7)\).
The sequence satisfies the linear recurrence:
\[a(n) = 2 a(n-1) - a(n-2) + a(n-5) - 2 a(n-6) + a(n-7)\]with initial values \(a(1) = 2, a(2) = 7, a(3) = 14, a(4) = 23, a(5) = 35, a(6) = 50, a(7) = 67\).
The sequence is 1-indexed in OEIS, so \(a(n)\) is the \((n-1)\)-th term of the 0-indexed solution.
References: - A227582 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/227582.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements and 1 API statement, counted here but not shown.
OeisA227582.a_eq_floor_harmonic_expr
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/227582.wip.lean#L282.
Conjecture (from A227581): \(a(n) = \lfloor 1/(2 H(n) - H(n^2 + n - 1) - \gamma) \rfloor\), where \(H\) denotes harmonic numbers and \(\gamma\) denotes the Euler-Mascheroni constant.
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_eq_floor_harmonic_expr (n : ℕ) (hn : 0 < n) :
a n = (Int.floor (1 / (2 * (↑(harmonic n) : ℝ) -
(↑(harmonic (n * n + n - 1)) : ℝ) - Real.eulerMascheroniConstant))).toNat
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/227582.lean, line 123.
Sources
TheoremRepresentations using Sophie Germain primes and twin prime pairs#
Number of ways to write \(n = x + y\) (\(x, y > 0\)) such that \(6x - 1\) is a Sophie Germain prime and \(\{6y - 1, 6y + 1\}\) is a twin prime pair.
References: - A227923
Quoted from FormalConjectures/OEIS/227923.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.
OeisA227923.conjecture_1
Open: stated without proof.
Conjecture (i), first part: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture_1 (n : ℕ) (hn : n > 1) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/227923.lean, line 61.
OeisA227923.conjecture_2
Open: stated without proof.
Conjecture (i), second part: Any integer \(n > 4\) not equal to \(13\) can be written as \(x + y\) with \(x\) and \(y\) distinct and greater than \(1\) such that \(6x - 1\) is a Sophie Germain prime and \(\{6y - 1, 6y + 1\}\) is a twin prime pair.
theorem conjecture_2 (n : ℕ) (hn : n > 4) (h13 : n ≠ 13) :
∃ x y : ℕ, 1 < x ∧ 1 < y ∧ x ≠ y ∧ x + y = n ∧
(6 * x - 1).Prime ∧ (12 * x - 1).Prime ∧
(6 * y - 1).Prime ∧ (6 * y + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/227923.lean, line 70.
OeisA227923.conjecture_3
Open: stated without proof.
Conjecture (ii), cousin prime variant: Any integer \(n > 1\) can be written as \(x + y\) (\(x, y > 0\)) such that \(6x - 1\) is a Sophie Germain prime and \(\{6y + 1, 6y + 5\}\) is a cousin prime pair.
theorem conjecture_3 (n : ℕ) (hn : n > 1) :
∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
(6 * x - 1).Prime ∧ (12 * x - 1).Prime ∧
(6 * y + 1).Prime ∧ (6 * y + 5).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/227923.lean, line 82.
OeisA227923.conjecture_4
Open: stated without proof.
Conjecture (ii), sexy prime variant: Any integer \(n > 1\) can be written as \(x + y\) (\(x, y > 0\)) such that \(6x - 1\) is a Sophie Germain prime and \(\{6y - 1, 6y + 5\}\) is a sexy prime pair.
theorem conjecture_4 (n : ℕ) (hn : n > 1) :
∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
(6 * x - 1).Prime ∧ (12 * x - 1).Prime ∧
(6 * y - 1).Prime ∧ (6 * y + 5).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/227923.lean, line 94.
Sources
TheoremEighth root of the generating function of an Apéry-like sequence#
The auxiliary sequence used for the Hankel matrix, defined as
\[\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2\]Determinant of the \((n+1) \times (n+1)\) Hankel-type matrix with \((i,j)\)-entry equal to A005259\((i+j)\) for all \(i,j = 0,\dots,n\). The entry function A005259 is taken to be \(\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2\).
References: - A228143 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - A005259
Quoted from FormalConjectures/OEIS/228143.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.
OeisA228143.exists_power_series_eighth_pow_eq
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/228143.wip.lean#L698.
Conjecture: if \(A(x) = 1 + 48x + 161856 x^2 + \cdots\) denotes the o.g.f. then \(A(x/3)^{1/8}\) has integer coefficients. - Peter Bala, Apr 22 2018
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem exists_power_series_eighth_pow_eq : ∃ C : PowerSeries ℤ,
(PowerSeries.map (Int.castRingHom ℚ)) (C ^ 8) = ogfAScaled
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228143.lean, line 99.
Sources
TheoremAlternating sum of fourth powers of binomial coefficients#
The sequence is defined by
\[a(n) = \sum_{k=0}^n \binom{n}{k}^4 (-1)^k.\]References: - A228304 - arXiv:2608.11941
Quoted from FormalConjectures/OEIS/228304.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.
OeisA228304.conjecture_1
Solved: stated here without proof.
Conjecture: Let \(p\) be any odd prime, and let \(A(p)\) be the \(p \times p\) determinant with \((i,j)\)-entry equal to \(a(i+j)\) for all \(i, j = 0, \dots, p-1\). Then \(A(p) \equiv (-1)^{(p-1)/2} \pmod p\).
Proved in arXiv:2608.11941.
theorem conjecture_1 (p : ℕ) (hp : p.Prime) (hodd : p ≠ 2) :
let A : Matrix (Fin p) (Fin p) ℤ := fun i j => a (i.val + j.val)
A.det ≡ (-1 : ℤ) ^ ((p - 1) / 2) [ZMOD p]
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228304.lean, line 72.
OeisA228304.conjecture_2
Solved: stated here without proof.
Conjecture: Let \(p\) be any odd prime, and let \(C(p)\) be the \(p \times p\) determinant with \((i,j)\)-entry equal to \(c(i+j)\) for all \(i, j = 0, \dots, p-1\). Then \(C(p) \equiv 1 \pmod p\).
Proved in arXiv:2608.11941.
theorem conjecture_2 (p : ℕ) (hp : p.Prime) (hodd : p ≠ 2) :
let C : Matrix (Fin p) (Fin p) ℤ := fun i j => c (i.val + j.val)
C.det ≡ 1 [ZMOD p]
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228304.lean, line 84.
Sources
TheoremPartitions of \(n\) into \(x + y\) with \(x(x+1)/2 + y^2\) prime#
Number of ways to write \(n = x + y\) (\(x, y > 0\)) with \(x(x+1)/2 + y^2\) prime.
References: - A228425
Quoted from FormalConjectures/OEIS/228425.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.
OeisA228425.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture_1 (n : ℕ) (hn : n > 1) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228425.lean, line 59.
OeisA228425.conjecture_2
Open: stated without proof.
We also conjecture that any integer \(n > 1\) can be written as \(x + y\) (\(x, y > 0\)) with \(p_k(x) + p_{k+1}(y)\) prime, if and only if \(k\) is among \(3, 39, 99\).
theorem conjecture_2 (k : ℕ) (hk : 3 ≤ k) :
(∀ n : ℕ, 1 < n → ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime (Nat.polygonalNumber k x + Nat.polygonalNumber (k + 1) y)) ↔
k = 3 ∨ k = 39 ∨ k = 99
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228425.lean, line 67.
OeisA228425.conjecture_3
Open: stated without proof.
The pair \((k, m)\) works if \(k\) is among \(3, 4, 6\), and \(m > k\) is not congruent to \(k\) modulo \(2\), in the sense that all sufficiently large integers \(n\) can be written as \(x + y\) (\(x, y > 0\)) with \(p_k(x) + p_m(y)\) prime. - Zhi-Wei Sun
theorem conjecture_3 (k m : ℕ) (hk : k = 3 ∨ k = 4 ∨ k = 6) (hm : k < m)
(hmod : ¬ m ≡ k [MOD 2]) :
∀ᶠ (n : ℕ) in Filter.atTop, ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime (Nat.polygonalNumber k x + Nat.polygonalNumber m y)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228425.lean, line 80.
OeisA228425.conjecture_4
Open: stated without proof.
For \(k = 5\), the pair \((5, m)\) works (with \(m > 5\)) if \(m\) is congruent to \(0\) or \(4\) modulo \(6\), in the sense that all sufficiently large integers \(n\) can be written as \(x + y\) (\(x, y > 0\)) with \(p_5(x) + p_m(y)\) prime. - Zhi-Wei Sun
theorem conjecture_4 (m : ℕ) (hm : 5 < m) (hmod : m ≡ 0 [MOD 6] ∨ m ≡ 4 [MOD 6]) :
∀ᶠ (n : ℕ) in Filter.atTop, ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime (Nat.polygonalNumber 5 x + Nat.polygonalNumber m y)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228425.lean, line 93.
OeisA228425.conjecture_5
Open: stated without proof.
The only pairs \((k, m)\) with \(2 < k \le 10\) and \(k < m \le 100\) such that any integer \(n > 1\) can be written as \(x + y\) (\(x, y > 0\)) with \(p_k(x) + p_m(y)\) prime, are the \(31\) pairs in
sunPolygonalPairs. - Zhi-Wei Sun
theorem conjecture_5 (k m : ℕ) (hk : 2 < k) (hk10 : k ≤ 10) (hm : k < m) (hm100 : m ≤ 100) :
(∀ n : ℕ, 1 < n → ∃ x y : ℕ, 0 < x ∧ 0 < y ∧ x + y = n ∧
Nat.Prime (Nat.polygonalNumber k x + Nat.polygonalNumber m y)) ↔
(k, m) ∈ sunPolygonalPairs
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228425.lean, line 115.
Sources
TheoremSquare root of the absolute value of the determinant of the prime sum indicator matrix#
Square root of the absolute value of \(\det(M_n)\), where \(M_n\) is the \(n \times n\) matrix with \((i,j)\)-entry (\(1 \le i, j \le n\)) equal to \(1\) if \(i + j\) is prime, and \(0\) otherwise.
References: - A228552
Quoted from FormalConjectures/OEIS/228552.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.
OeisA228552.conjecture
Open: stated without proof.
We conjecture that \(a(n) > 0\) for all \(n > 15\).
theorem conjecture (n : ℕ) (hn : n > 15) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228552.lean, line 64.
Sources
TheoremDeterminant of odd composite sum indicator matrix#
Determinant of the \(n \times n\) \((0,1)\)-matrix with \((i,j)\)-entry (\(1 \le i, j \le n\)) equal to \(1\) if and only if \(i + j\) is \(2\) or an odd composite number.
References: - A228591
Quoted from FormalConjectures/OEIS/228591.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.
OeisA228591.conjecture
Open: stated without proof.
Conjecture: \(a(n) = 0\) for no \(n > 15\).
theorem conjecture (n : ℕ) (hn : n > 15) : a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228591.lean, line 80.
Sources
TheoremDeterminant of prime sum/difference matrix#
Determinant of the \(n \times n\) matrix with \((i,j)\)-entry (\(i, j = 0, \dots, n - 1\)) equal to \(1\) or \(0\) according as \(n + i - j\) and \(n - i + j\) are both prime or not.
References: - A228623
Quoted from FormalConjectures/OEIS/228623.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.
OeisA228623.conjecture
Open: stated without proof.
Conjecture: \(a(n)\) is nonzero if \(n\) is odd and greater than \(120\).
theorem conjecture (n : ℕ) (hn : n > 120) (hodd : Odd n) : a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228623.lean, line 90.
Sources
TheoremDeterminant of square/cube sum matrix#
Determinant of the \(n \times n\) matrix with \((i,j)\)-entry (\(i, j = 1, \dots, n\)) equal to \(1\) or \(0\) according as \(i + j\) is a square or not.
References: - A228624
Quoted from FormalConjectures/OEIS/228624.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.
OeisA228624.conjecture_1
Open: stated without proof.
Conjecture: \(a(n)\) is nonzero for any \(n > 21\).
theorem conjecture_1 (n : ℕ) (hn : n > 21) : a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228624.lean, line 71.
OeisA228624.conjecture_2
Open: stated without proof.
Conjecture: Let \(A(n)\) be the \(n \times n\) determinant with \((i,j)\)-entry equal to \(1\) or \(0\) according as \(i + j\) is a cube or not. Then \(A(n)\) is nonzero for any \(n > 176\). - Zhi-Wei Sun
theorem conjecture_2 (n : ℕ) (hn : n > 176) : b n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228624.lean, line 81.
Sources
TheoremNumbers \(n\) such that \(n^2 + \pi(n)\) is prime#
References: - A228828
Quoted from FormalConjectures/OEIS/228828.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 3 test statements, counted here but not shown.
OeisA228828.conjecture
Open: stated without proof.
Conjecture: the sequence A228828 is infinite.
theorem conjecture : {a n | n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/228828.lean, line 68.
Sources
TheoremUndirected circular permutations with adjacent products minus one all prime#
Number of undirected circular permutations \(\pi(1), \dots, \pi(n)\) of \(1, \dots, n\) with the \(n\) numbers \(\pi(1)\pi(2)-1, \pi(2)\pi(3)-1, \dots, \pi(n-1)\pi(n)-1, \pi(n)\pi(1)-1\) all prime.
References: - A229232
Quoted from FormalConjectures/OEIS/229232.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 6 test statements, counted here but not shown.
OeisA229232.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 5\) with \(n\) not equal to \(13\).
theorem conjecture_1 (n : ℕ) (hn : n > 5) (hne : n ≠ 13) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229232.lean, line 67.
OeisA229232.conjecture_2
Open: stated without proof.
Conjecture: For any integer \(n > 1\), there is a permutation \(\pi(1), \dots, \pi(n)\) of \(1, \dots, n\) such that the \(n\) numbers \(2\pi(1)\pi(2)-1, \dots, 2\pi(n-1)\pi(n)-1, 2\pi(n)\pi(1)-1\) are all prime. - Zhi-Wei Sun
theorem conjecture_2 (n : ℕ) (hn : n > 1) :
∃ π : Equiv.Perm (Fin n), ∀ i : Fin n,
(2 * ((π i).val + 1) *
((π ⟨(i.val + 1) % n, Nat.mod_lt _ (by omega)⟩).val + 1) - 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229232.lean, line 77.
OeisA229232.conjecture_3
Open: stated without proof.
Conjecture: For any positive integer \(n\) not equal to \(4\), there is a permutation \(\pi(1), \dots, \pi(n)\) of \(1, \dots, n\) such that the \(n\) numbers \(2\pi(1)\pi(2)+1, \dots, 2\pi(n-1)\pi(n)+1, 2\pi(n)\pi(1)+1\) are all prime. - Zhi-Wei Sun
theorem conjecture_3 (n : ℕ) (hn : n > 0) (hne : n ≠ 4) :
∃ π : Equiv.Perm (Fin n), ∀ i : Fin n,
(2 * ((π i).val + 1) * ((π ⟨(i.val + 1) % n, Nat.mod_lt _ hn⟩).val + 1) + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229232.lean, line 90.
OeisA229232.conjecture_4
Open: stated without proof.
Conjecture: Let \(F\) be a finite field with \(q > 7\) elements. Then, there is a circular permutation \(a_1, \dots, a_{q-1}\) of the \(q-1\) nonzero elements of \(F\) such that all the \(q-1\) elements \(a_1 a_2 - 1, a_2 a_3 - 1, \dots, a_{q-2} a_{q-1} - 1, a_{q-1} a_1 - 1\) are primitive elements of the field \(F\) (i.e., generators of the multiplicative group \(F \setminus \{0\}\)). - Zhi-Wei Sun
theorem conjecture_4 (F : Type*) [Field F] [Fintype F] (hF : Fintype.card F > 7) :
let m := Fintype.card F - 1
∃ a : Fin m ≃ Fˣ,
∀ i : Fin m, IsPrimitiveRoot
((a i : F) * (a ⟨(i.val + 1) % m, Nat.mod_lt _ (by omega)⟩ : F) - 1) m
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/229232.lean, line 104.
OeisA229232.conjecture_5
Open: stated without proof.
Conjecture: Let \(F\) be a finite field with \(q > 7\) elements. There is a circular permutation \(b_1, \dots, b_{q-1}\) of the \(q-1\) nonzero elements of \(F\) such that all the \(q-1\) elements \(b_1 b_2 + 1, b_2 b_3 + 1, \dots, b_{q-2} b_{q-1} + 1, b_{q-1} b_1 + 1\) are primitive elements of the field \(F\) (i.e., generators of the multiplicative group \(F \setminus \{0\}\)). - Zhi-Wei Sun
theorem conjecture_5 (F : Type*) [Field F] [Fintype F] (hF : Fintype.card F > 7) :
let m := Fintype.card F - 1
∃ b : Fin m ≃ Fˣ,
∀ i : Fin m, IsPrimitiveRoot
((b i : F) * (b ⟨(i.val + 1) % m, Nat.mod_lt _ (by omega)⟩ : F) + 1) m
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/229232.lean, line 119.
Sources
TheoremWays to write \(n = x + y + z\) with six linear and quadratic forms prime#
Number of ways to write \(n = x + y + z\) with \(0 < x \le y \le z\) such that all the six numbers \(2x-1, 2y-1, 2z-1, 2xy-1, 2xz-1, 2yz-1\) are prime.
References: - A229969
Quoted from FormalConjectures/OEIS/229969.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 open. It also has 7 test statements, counted here but not shown.
OeisA229969.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 5\).
theorem conjecture_1 (n : ℕ) (hn : n > 5) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 69.
OeisA229969.conjecture_2
Open: stated without proof.
Moreover, any integer \(n > 6\) can be written as \(x + y + z\) with \(x\) among \(3, 4, 6, 10, 15\) such that \(2y-1, 2z-1, 2xy-1, 2xz-1, 2yz-1\) are prime.
theorem conjecture_2 (n : ℕ) (hn : n > 6) :
∃ x y z : ℕ, 0 < y ∧ 0 < z ∧ x + y + z = n ∧
x ∈ ({3, 4, 6, 10, 15} : Finset ℕ) ∧
(2 * y - 1).Prime ∧ (2 * z - 1).Prime ∧
(2 * x * y - 1).Prime ∧ (2 * x * z - 1).Prime ∧ (2 * y * z - 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 77.
OeisA229969.conjecture_3a
Open: stated without proof.
Conjecture (i), part 1: Any integer \(n > 6\) can be written as \(x + y + z\) (\(x, y, z > 0\)) with \(2x-1, 2y-1, 2z-1\) and \(2xyz-1\) all prime and \(x\) among \(2, 3, 4\). - Zhi-Wei Sun
theorem conjecture_3a (n : ℕ) (hn : n > 6) :
∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧ x + y + z = n ∧
x ∈ ({2, 3, 4} : Finset ℕ) ∧
(2 * x - 1).Prime ∧ (2 * y - 1).Prime ∧ (2 * z - 1).Prime ∧
(2 * x * y * z - 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 90.
OeisA229969.conjecture_3b
Open: stated without proof.
Conjecture (i), part 2: Each integer \(n > 2\) can be written as \(x + y + z\) (\(x, y, z > 0\)) with \(2x+1, 2y+1, 2z+1\) and \(2xyz+1\) all prime and \(x\) among \(1, 2, 3\). - Zhi-Wei Sun
theorem conjecture_3b (n : ℕ) (hn : n > 2) :
∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧ x + y + z = n ∧
x ∈ ({1, 2, 3} : Finset ℕ) ∧
(2 * x + 1).Prime ∧ (2 * y + 1).Prime ∧ (2 * z + 1).Prime ∧
(2 * x * y * z + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 103.
OeisA229969.conjecture_4
Open: stated without proof.
Conjecture (ii): Each integer \(n > 4\) can be written as \(x + y + z\) with \(x = 3\) or \(6\) such that \(2y+1, 2xyz-1\) and \(2xyz+1\) are prime. - Zhi-Wei Sun
theorem conjecture_4 (n : ℕ) (hn : n > 4) :
∃ x y z : ℕ, 0 < y ∧ 0 < z ∧ x + y + z = n ∧
(x = 3 ∨ x = 6) ∧
(2 * y + 1).Prime ∧ (2 * x * y * z - 1).Prime ∧ (2 * x * y * z + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 116.
OeisA229969.conjecture_5a
Open: stated without proof.
Conjecture (iii), part 1: Every integer \(n > 5\) can be written as \(x + y + z\) (\(x, y, z > 0\)) with \(xy-1, xz-1, yz-1\) all prime and \(x\) among \(2, 6, 10\). - Zhi-Wei Sun
theorem conjecture_5a (n : ℕ) (hn : n > 5) :
∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧ x + y + z = n ∧
x ∈ ({2, 6, 10} : Finset ℕ) ∧
(x * y - 1).Prime ∧ (x * z - 1).Prime ∧ (y * z - 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 128.
OeisA229969.conjecture_5b
Open: stated without proof.
Conjecture (iii), part 2: Any integer \(n > 2\) not equal to \(16\) can be written as \(x + y + z\) (\(x, y, z > 0\)) with \(xy+1, xz+1, yz+1\) all prime and \(x\) among \(1, 2, 6\). - Zhi-Wei Sun
theorem conjecture_5b (n : ℕ) (hn : n > 2) (hne : n ≠ 16) :
∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧ x + y + z = n ∧
x ∈ ({1, 2, 6} : Finset ℕ) ∧
(x * y + 1).Prime ∧ (x * z + 1).Prime ∧ (y * z + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/229969.lean, line 140.
Sources
TheoremPartitions \(n = p + q\) with \(p\), \(3p - 10\), and \((p - 1)q - 1\) prime#
Number of ways to write \(n = p + q\) with \(p\), \(3p - 10\) and \((p-1)q - 1\) all prime, where \(q\) is a positive integer.
References: - A230241
Quoted from FormalConjectures/OEIS/230241.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 7 test statements, counted here but not shown.
OeisA230241.conjecture
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 5\).
theorem conjecture (n : ℕ) (hn : n > 5) : a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/230241.lean, line 65.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.