Conjectures associated with… to Number of prime powers strictly…
TheoremConjectures associated with A067720#
A067720 lists numbers \(k\) such that \(\varphi(k^2 + 1) = k \cdot \varphi(k + 1)\), where \(\varphi\) is Euler's totient function.
The sequence exhibits a strong connection to primes: for almost all terms \(k\), \(k + 1\) is prime. The conjecture states that \(k = 8\) is the only exception.
References: - A067720
Quoted from FormalConjectures/OEIS/67720.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 1 open and 1 textbook result. It also has 6 test statements, counted here but not shown.
OeisA67720.a_of_primes
Textbook result, proved here.
If \(k + 1\) and \(k^2 + 1\) are both prime, then \(k\) is in the sequence.
theorem a_of_primes {k : ℕ} (hk : (k + 1).Prime) (hk' : (k ^ 2 + 1).Prime) : A k
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/67720.lean, line 74.
OeisA67720.prime_add_one_of_a
Open: stated without proof.
For members of the sequence other than \(8\), we have \(k + 1\) is prime.
theorem prime_add_one_of_a {k : ℕ} (h : A k) (hne : k ≠ 8) : (k + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/67720.lean, line 79.
Sources
TheoremEuclid–Fortunate prime coverage#
OEIS A067836 starts with \(2\). Each later term is the gap from the product of all previous terms to the least prime strictly greater than that product plus one.
References: - OEIS A067836
Quoted from FormalConjectures/OEIS/67836.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 and 5 API statements, counted here but not shown.
OeisA67836.conjecture
Open: stated without proof.
OEIS A067836 asks: "Do all primes occur in the sequence?"
theorem conjecture :
∀ p, p.Prime → ∃ n ≥ 1, a n = p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/67836.lean, line 138.
Sources
TheoremSum of \(a(k)/k!\) over divisors equals harmonic number#
The sequence \(a(n)\) satisfies \(\sum_{k \mid n} \frac{a(k)}{k!} = \sum_{j=1}^n \frac{1}{j} = H_n\), where the sum on the left is over positive divisors \(k\) of \(n\). By Möbius inversion,
\[a(n) = n! \sum_{d \mid n} \mu(n/d) H_d\]where \(H_d = \sum_{j=1}^d \frac{1}{j}\) is the \(d\)-th harmonic number.
Quoted from FormalConjectures/OEIS/67857.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.
OeisA67857.conjecture
Solved: stated here; a Lean proof is at https://github.com/SamuelSchlesinger/a067857-counterexample/blob/44317ddb5bd735f7a1f6764c22db10c455e4b584/Counterexample.lean#L89-L92.
The terms are not all positive. The first negative one is \(a(30) = -22690644647302814715858124800000\). Conjecture: \(a(n) < 0\) if and only if A001221(n) is an odd number \(\ge 3\).
This conjecture is false. A counterexample is the product of all primes at most \(1000\), which has \(168\) distinct prime factors and a negative sequence value.
The counterexample and formal proof were developed by Codex (GPT-6), prompted by Samuel Schlesinger.
theorem conjecture :
¬ ∀ n : ℕ, 0 < n →
(a n < 0 ↔ Odd (cardDistinctFactors n) ∧ 3 ≤ cardDistinctFactors n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/67857.lean, line 86.
Sources
TheoremNumber of times \(n^2 + s^2\) is prime for positive integers \(s < n\)#
The sequence \(a(n)\) counts the number of integers \(s \in \{1, \dots, n-1\}\) such that \(n^2 + s^2\) is prime:
\[a(n) = \sum_{s=1}^{n-1} [\text{Prime}(n^2 + s^2)]\]References: - A069004 - [CE26] j2d9w5xtjn-png, Counterexample to the upper bound, 2026. - [Li26] Wentao Li, Lean certificate for the A069004 counterexample, 2026.
Quoted from FormalConjectures/OEIS/69004.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 5 test statements, counted here but not shown.
OeisA69004.conjecture1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture1 (n : ℕ) (hn : 1 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69004.lean, line 71.
OeisA69004.conjecture2
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/a16a2711b082ccab4ba941330148e7b7c78b11c1/LeanOeisProofs/NewFormalization/A069004.lean#L58.
Stronger conjecture: Let pi(n) be the prime counting function (A000720). Then pi(n) >= a(n) >= pi(n)/5 for n>1, with the following equalities: pi(2)=a(2), pi(10)=a(10) and a(12)=pi(12)/5. - T. D. Noe, Feb 26 2007
This conjunction is false. The upper bound fails at \(n = 512720\): a Lean certificate proves \(a(512720) \ge 42494 > 42493 = \pi(512720)\). The counterexample was recorded by j2d9w5xtjn-png [CE26].
Lean formalization by Wentao Li, with AI assistance, adapting Epoch Research's certificate attempt; see [Li26].
theorem conjecture2 : ¬ (
(∀ n : ℕ, 1 < n → Nat.primeCounting n ≥ a n) ∧
(∀ n : ℕ, 1 < n → 5 * a n ≥ Nat.primeCounting n) ∧
Nat.primeCounting 2 = a 2 ∧
Nat.primeCounting 10 = a 10 ∧
5 * a 12 = Nat.primeCounting 12)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69004.lean, line 90.
OeisA69004.conjecture2.variants.upper_bound_false
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/a16a2711b082ccab4ba941330148e7b7c78b11c1/LeanOeisProofs/NewFormalization/A069004.lean#L49.
The upper bound from T. D. Noe's stronger conjecture: "pi(n) >= a(n)" for "n>1". It is false at \(n = 512720\): \(a(512720) \ge 42494 > 42493 = \pi(512720)\). The counterexample was recorded by j2d9w5xtjn-png [CE26].
Lean formalization by Wentao Li, with AI assistance, adapting Epoch Research's certificate attempt; see [Li26].
theorem conjecture2.variants.upper_bound_false :
¬ ∀ n : ℕ, 1 < n → Nat.primeCounting n ≥ a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69004.lean, line 109.
OeisA69004.conjecture2.variants.without_upper_bound
Open: stated without proof.
The part of the stronger conjecture that survives the counterexample to its upper bound: \(5 a(n) \ge \pi(n)\) for \(n > 1\), together with the three claimed equalities \(\pi(2) = a(2)\), \(\pi(10) = a(10)\) and \(a(12) = \pi(12)/5\).
theorem conjecture2.variants.without_upper_bound :
(∀ n : ℕ, 1 < n → 5 * a n ≥ Nat.primeCounting n) ∧
Nat.primeCounting 2 = a 2 ∧
Nat.primeCounting 10 = a 10 ∧
5 * a 12 = Nat.primeCounting 12
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69004.lean, line 118.
Sources
TheoremDeterminant of prime sum indicator matrix#
Determinant of 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: - A069191
Quoted from FormalConjectures/OEIS/69191.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.
OeisA69191.conjecture_1
Open: stated without proof.
Conjecture: Let \(M(n)\) be the \(n \times n\) matrix with \((i,j)\)-entry equal to \(1\) or \(0\) according as \(i + j\) is prime or not. For each \(n = 24, 25, \dots\), the characteristic polynomial of \(M(n)\) is irreducible over the field of rational numbers. - Zhi-Wei Sun, Aug 25 2013
theorem conjecture_1 (n : ℕ) (hn : 24 ≤ n) :
Irreducible (primeMatrix ℚ n).charpoly
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69191.lean, line 107.
OeisA69191.conjecture_2
Open: stated without proof.
Conjecture: Let \(M(n)\) be the \(n \times n\) matrix with \((i,j)\)-entry equal to \(1\) or \(0\) according as \(i + j\) is prime or not. For each \(n = 24, 25, \dots\), the \(n\) eigenvalues of \(M(n)\) can be listed as \(\lambda(1), \dots, \lambda(n)\) such that \(\lambda(1) > -\lambda(2) > \lambda(3) > -\lambda(4) > \dots > (-1)^{n-1} \lambda(n) > 0\). - Zhi-Wei Sun, Aug 25 2013
theorem conjecture_2 (n : ℕ) (hn : 24 ≤ n) :
∃ ev : Fin n → ℝ,
(primeMatrix ℝ n).charpoly = ∏ i : Fin n, (Polynomial.X - Polynomial.C (ev i)) ∧
StrictAnti (fun i : Fin n => (-1 : ℝ) ^ (i : ℕ) * ev i) ∧
∀ i : Fin n, 0 < (-1 : ℝ) ^ (i : ℕ) * ev i
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69191.lean, line 119.
Sources
TheoremNumber of primes \(p\) such that \(n^n \le p \le n^n + n^2\)#
The sequence \(a(n)\) counts the number of prime numbers in the interval \([n^n, n^n + n^2]\):
\[a(n) = |\{p \text{ prime} \mid n^n \le p \le n^n + n^2\}|\]References: - A069922
Quoted from FormalConjectures/OEIS/69922.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.
OeisA69922.conjecture
Open: stated without proof.
Question: for any \(n > 0\), is there at least one prime \(p\) such that \(n^n \le p \le n^n + n^2\)? In this case, that would be stronger than the Schinzel conjecture: "for \(m > 1\) there's at least one prime \(p\) such that \(m \le p \le m + \log(m)^2\)" since \(n^2 < \log(n^n)^2 = n^2 \log(n)^2\).
theorem conjecture (n : ℕ) (hn : 0 < n) : 1 ≤ a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69922.lean, line 69.
Sources
TheoremNumber of primes \(p\) such that \(2^n \le p \le 2^n + \mathrm{prime}(n)\)#
The sequence \(a(n)\) counts the number of primes \(p\) in the interval \([2^n, 2^n + p_n]\), where \(p_n\) is the \(n\)-th prime (\(p_1 = 2, p_2 = 3, \dots\)):
\[a(n) = |\{p \text{ prime} \mid 2^n \le p \le 2^n + p_n\}|\]for \(n \ge 1\), and \(a(0) = 0\).
References: - A069923
Quoted from FormalConjectures/OEIS/69923.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.
OeisA69923.conjecture
Open: stated without proof.
For any \(n > 0\), is there always at least one prime \(p\) such that \(2^n \le p \le 2^n + \mathrm{prime}(n)\)? (checked up to \(n = 250\)). In this case, that would be stronger than the Schinzel conjecture: "for \(m > 1\) there's at least one prime \(p\) such that \(m \le p \le m + \log(m)^2\)" since, for \(n > 2\), \(\mathrm{prime}(n) < \log(2^n)^2 = n^2 \log(2)\).
theorem conjecture (n : ℕ) (hn : 0 < n) : 1 ≤ a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/69923.lean, line 79.
Sources
TheoremValue of \(n\)-th cyclotomic polynomial at \(n\)#
The sequence \(a(n) = \Phi_n(n)\) gives the value of the \(n\)-th cyclotomic polynomial evaluated at \(n\):
\[a(n) = |\Phi_n(n)|\]References: - A070518
Quoted from FormalConjectures/OEIS/70518.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.
OeisA70518.conjecture
Open: stated without proof.
\(a(28341)\) is divisible by \(283411^2\). What is the next \(n\) such that \(a(n)\) is not squarefree?
theorem conjecture :
conjecture.answer =
if h : ∃ n, 28341 < n ∧ ¬ Squarefree (a n) then
some (sInf {n | 28341 < n ∧ ¬ Squarefree (a n)})
else
none
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/70518.lean, line 77.
Sources
TheoremRecurrence \(a(n+2) = |a(n+1)a(n) - a(n)a(n+1)|\) via concatenation#
The sequence starts with \(a(1) = 0, a(2) = 1\). For \(n \ge 1\),
\[a(n+2) = |\text{concat}(a(n+1), a(n)) - \text{concat}(a(n), a(n+1))|\]where concatenation is in decimal representation.
References: - A070823
Quoted from FormalConjectures/OEIS/70823.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.
OeisA70823.conjecture
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a070823-counterexample/blob/51399770e734616c6463be034e41f7469991d752/lean/OeisA70823CounterexampleFC.lean#L72-L81.
\(a(n) \equiv 0 \pmod 3\) if \(n > 2\). Is \(a(n)\) always of the form \(2^j \cdot 3^k \cdot s\) where \(s\) is a squarefree number?
Answer: False, \(a(20)\) is divisible by \(13^2\) but not by \(13^3\).
theorem conjecture :
¬ ∀ n : ℕ, 2 < n →
a n ≡ 0 [MOD 3] ∧
∃ j k s : ℕ, a n = 2 ^ j * 3 ^ k * s ∧ Squarefree s
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/70823.lean, line 88.
Sources
TheoremDeterminant of matrix with entries indicating primality of \(i^2 + j^2\)#
The sequence \(a(n)\) is the determinant of the \(n \times n\) matrix \(M\) defined by \(M(i,j) = 1\) if \(i^2 + j^2\) is prime, and \(0\) otherwise, where \(1 \le i, j \le n\).
References: - A071524
Quoted from FormalConjectures/OEIS/71524.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.
OeisA71524.conjecture1
Open: stated without proof.
Conjecture: \(a(n) = 0\) for no \(n > 28\). - Zhi-Wei Sun, Aug 26 2013
theorem conjecture1 (n : ℕ) (hn : 28 < n) : a n ≠ 0
Category research open; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/71524.lean, line 85.
OeisA71524.conjecture2
Open: stated without proof.
Conjecture (Generalization): For every \(m \in \mathbb{N}\), the determinant
generalDet m nis nonzero for all sufficiently large \(n\). - Zhi-Wei Sun, Aug 26-27 2013
theorem conjecture2 (m : ℕ) : ∃ N : ℕ, ∀ n : ℕ, N < n → generalDet m n ≠ 0
Category research open; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/71524.lean, line 94.
Sources
TheoremAlternating sum of signs of powers of \(3/2\)#
The sequence \(a(n) = -\sum_{k=1}^n (-1)^{\lfloor (3/2)^k \rfloor}\).
References: - A071532
Quoted from FormalConjectures/OEIS/71532.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 3 open and 1 solved. It also has 5 test statements, counted here but not shown.
OeisA71532.conjecture1
Solved: stated here; a Lean proof is at https://github.com/SamuelSchlesinger/a071532-counterexample/blob/818c9f6b3f1eed9ebd1b3b9481848dc21f3e3243/Counterexample.lean#L28-L35.
"Is \(a(n)>0\)?"
The answer is negative: \(a(331523) = -1\). The restriction \(n > 2\) excludes the initial zero \(a(2) = 0\).
The counterexample and formal proof were developed by Codex (GPT-6), prompted by Samuel Schlesinger.
theorem conjecture1 : ¬ ∀ n : ℕ, 2 < n → 0 < a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/71532.lean, line 76.
OeisA71532.conjecture2
Open: stated without proof.
For \(n\) large enough, does \(a(n) > \sqrt{n}\) always hold?
theorem conjecture2 :
∃ N : ℕ, ∀ n : ℕ, N ≤ n → (a n : ℝ) > Real.sqrt (n : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/71532.lean, line 83.
OeisA71532.conjecture3
Open: stated without proof.
Conjecture: asymptotically, \(a(n) \sim C \log(n)^2\) for some constant \(C > 0\).
theorem conjecture3 :
∃ C : ℝ, 0 < C ∧ (fun n : ℕ ↦ (a n : ℝ)) ~[atTop] (fun n : ℕ ↦ C * Real.log (n : ℝ) ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/71532.lean, line 91.
OeisA71532.conjecture3_value
Open: stated without proof.
Conjecture: the constant \(C\) in \(a(n) \sim C \log(n)^2\) is approximately \(1.4\).
theorem conjecture3_value :
|conjecture3_value.answer - 1.4| < 0.1 ∧
(fun n : ℕ ↦ (a n : ℝ)) ~[atTop] (fun n : ℕ ↦ conjecture3_value.answer * Real.log (n : ℝ) ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/71532.lean, line 101.
Sources
TheoremSmallest factorial containing exactly \(n\) 6's#
The sequence \(a(n)\) gives the smallest \(k\) such that the decimal expansion of \(k!\) contains exactly \(n\) occurrences of the digit '6', or \(0\) if no such \(k\) exists.
References: - A072200
Quoted from FormalConjectures/OEIS/72200.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.
OeisA72200.conjecture
Open: stated without proof.
It is conjectured that \(a(24) = 0\) since no factorial less than \(10000\) contained just 24 sixes.
theorem conjecture : a 24 = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/72200.lean, line 95.
Sources
TheoremNumber of times \(n\) occurs as a binary sub-pattern of \(n^2\)#
The sequence \(a(n)\) is the number of times the binary expansion of \(n\) appears as a contiguous sublist (infix) in the binary expansion of \(n^2\).
References: - A076141
Quoted from FormalConjectures/OEIS/76141.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 6 test statements, counted here but not shown.
OeisA76141.conjecture
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a076141-binary-word/blob/b4e179767fa3041c43e019b559ee77e6737317aa/lean/OeisA76141FC.lean#L1229-L1253.
Is \(a(n) \le 1\) for all \(n\)?
theorem conjecture (n : ℕ) : a n ≤ 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/76141.lean, line 81.
Sources
TheoremSmallest \(x\) such that \(\sigma(x) \bmod x = n\)#
The sequence \(a(n)\) is the smallest positive integer \(x\) such that \(\sigma_1(x) \bmod x = n\), or \(0\) if no such \(x\) exists.
References: - A076495
Quoted from FormalConjectures/OEIS/76495.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.
OeisA76495.conjecture
Open: stated without proof.
At present, the 0 entry for \(n = 5\) is only a conjecture. That is, it is conjectured that there is no positive integer \(x\) such that \(\sigma_1(x) \bmod x = 5\).
theorem conjecture : a 5 = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/76495.lean, line 101.
Sources
TheoremTrajectory of 103 under the Reverse and Add! operation in base 3#
The sequence \(a(n)\) is the trajectory of \(103\) under the Reverse and Add! operation carried out in base \(3\), written in base \(10\). \(a(0) = 103\), and \(a(n+1) = a(n) + \text{rev}_3(a(n))\).
References: - A077408
Quoted from FormalConjectures/OEIS/77408.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.
OeisA77408.conjecture
Open: stated without proof.
\(103\) is conjectured to be the smallest number such that the Reverse and Add! algorithm in base \(3\) does not lead to a palindrome. Its trajectory is conjectured to never reach a palindrome.
theorem conjecture (n : ℕ) : ¬ IsBasePalindrome 3 (a n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/77408.lean, line 83.
Sources
Theorem\(a(1)=1, a(2)=1, a(n)=(2^{a(n-1)} + 1)/a(n-2)\)#
The sequence is defined by \(a(1) = 1, a(2) = 1\), and for \(n \ge 3\),
\[a(n) = \frac{2^{a(n-1)} + 1}{a(n-2)}\]References: - A078590
Quoted from FormalConjectures/OEIS/78590.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.
OeisA78590.conjecture
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a078590-counterexample/blob/3bdf1cee8e7e4cbc4fe83354e4be8ca1eee46de3/lean/OeisA78590CounterexampleFC.lean#L55-L61.
Are all terms integers?
No. Exact divisibility first fails at \(n = 7\); the corresponding rational term has reduced denominator \(19\).
theorem conjecture :
¬ ∀ n : ℕ, 3 ≤ n → a (n - 2) ∣ 2 ^ a (n - 1) + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/78590.lean, line 75.
Sources
TheoremSmallest \(m > 0\) such that \(n \cdot 2^m + 1\) is prime#
The sequence \(a(n)\) is the smallest positive integer \(m\) such that \(n \cdot 2^m + 1\) is prime, or \(0\) if no such \(m\) exists.
References: - A078680
Quoted from FormalConjectures/OEIS/78680.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.
OeisA78680.conjecture
Open: stated without proof.
There is a conjecture that the first zero is \(n = 65536 = 2^{16}\) (which is equivalent to the statement that \(2^{2^k} + 1\) is composite for \(k > 4\)). - T. D. Noe, Feb 25 2011
theorem conjecture :
a (2 ^ 16) = 0 ∧ ∀ n : ℕ, 1 ≤ n ∧ n < 2 ^ 16 → a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/78680.lean, line 96.
Sources
TheoremLeast \(k > 0\) such that \((k+1)(k+2)\cdots(k+n) + 1\) is prime#
The sequence \(a(n)\) is the least positive integer \(k\) such that \((k+1)(k+2)\cdots(k+n) + 1\) is prime, if such \(k\) exists; otherwise \(a(n) = 0\).
References: - A078729
Quoted from FormalConjectures/OEIS/78729.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.
OeisA78729.conjecture
Open: stated without proof.
\((k+1)(k+2)(k+3)(k+4) + 1 = (k^2 + 5k + 5)^2\), which is never prime. Hence \(a(4) = 0\). Conjecture: \(a(n) = 0\) if and only if \(n = 4\).
theorem conjecture (n : ℕ) (hn : 0 < n) : a n = 0 ↔ n = 4
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/78729.lean, line 101.
Sources
Theorem\(a(n) = \sum_{k=0}^n \binom{2k}{k}^3\)#
The sequence \(a(n) = 1 + \binom{2}{1}^3 + \binom{4}{2}^3 + \cdots + \binom{2n}{n}^3\):
\[a(n) = \sum_{k=0}^n \binom{2k}{k}^3\]References: - A079727
Quoted from FormalConjectures/OEIS/79727.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.
OeisA79727.conjecture1
Open: stated without proof.
Conjecture 1 (Peter Bala, 2024): If prime \(p\) is in A003625 then \(a(p^2) \equiv 8 + p^2 \pmod{p^3}\).
theorem conjecture1 (p : ℕ) (hp : OeisA3625.A p) :
a (p ^ 2) ≡ 8 + p ^ 2 [MOD p ^ 3]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/79727.lean, line 68.
OeisA79727.conjecture2
Open: stated without proof.
Conjecture 2 (Peter Bala, 2024): If prime \(p\) is in A003625 then \(a(p(p-1)) \equiv p^2 \pmod{p^3}\).
theorem conjecture2 (p : ℕ) (hp : OeisA3625.A p) :
a (p * (p - 1)) ≡ p ^ 2 [MOD p ^ 3]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/79727.lean, line 77.
OeisA79727.conjecture3
Open: stated without proof.
Conjecture 3 (Peter Bala, 2024): If prime \(p\) is in A003625 then \(a((p^2-1)/2) \equiv p^2 \pmod{p^4}\).
theorem conjecture3 (p : ℕ) (hp : OeisA3625.A p) :
a ((p ^ 2 - 1) / 2) ≡ p ^ 2 [MOD p ^ 4]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/79727.lean, line 86.
OeisA79727.conjecture4
Open: stated without proof.
Conjecture 4 (Peter Bala, 2024): If \(n\) is a product of distinct primes from A003625 then \(a((n-1)/2)\) is divisible by \(n^2\).
theorem conjecture4 (S : Finset ℕ) (hS : ∀ p ∈ S, OeisA3625.A p) :
(∏ p ∈ S, p) ^ 2 ∣ a ((∏ p ∈ S, p - 1) / 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/79727.lean, line 95.
Sources
TheoremNumber of prime powers strictly between \(n\)-th prime and \((n+1)\)-th prime#
The sequence \(a(n)\) is the number of prime powers \(k\) strictly between the \(n\)-th prime \(p_n\) and the \((n+1)\)-th prime \(p_{n+1}\): \(p_n < k < p_{n+1}\).
References: - A080101
Quoted from FormalConjectures/OEIS/80101.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 4 test statements, counted here but not shown.
OeisA80101.conjecture
Open: stated without proof.
It is conjectured that \(a(n) \le 2\) for all \(n\).
theorem conjecture (n : ℕ) : a n ≤ 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/80101.lean, line 74.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.