Conjecture relating two… to Prime-th recurrence with…
TheoremConjecture relating two characterizations of a set of integers.#
Informal Statement: For an integer \(k \ge 2\), the following are equivalent:
The greatest common divisor of the binomial coefficients \(\binom{2k}{k}, \binom{3k}{k}, \dots, \binom{(k+1)k}{k} = 1\).
Writing prime factorization of \(k\) as \(k = \prod p_i^{e_i}\), and let \(P = \max_i p_i^{e_i}\), one has \(k / P > P\).
This conjecture asserts that the sequence defined by 1. is obtained by taking 1 off each number in the sequence defined by 2.
Quoted from FormalConjectures/OEIS/80170.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.
OeisA80170.gcdCondition_iff_primePowerCondition
Solved: stated here; a Lean proof is at https://github.com/guodk/formal-conjectures/blob/0720658844d76a50d48e4baa152eef14d4462907/FormalConjectures/OEIS/80170.lean#L1823.
Conjecture: The gcd condition is equivalent to the prime power condition. This has been conjectured by Ralf Stephan.
Both the natural-language proof and its Lean 4 formalization were carried out by the KLMM MechMath Agent Team; see the
formal_proofattribute.References: - Ralf Stephan, Prove or Disprove. 100 Conjectures from the OEIS, 2004, Conjecture 17 (arXiv:math/0409509) - Dakai Guo et al., A Greatest Common Divisor Criterion of Certain Binomial Coefficients, 2026 (arXiv:2606.22997)
theorem gcdCondition_iff_primePowerCondition (k : ℕ) (hk : 2 ≤ k) :
A k ↔ B (k + 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/80170.lean, line 91.
Sources
TheoremDenominator of \(\sum_{k=1}^n k^{\mu(k)}\)#
The sequence \(a(n)\) is the denominator of \(\sum_{k=1}^n k^{\mu(k)}\), where \(\mu\) is the Möbius function.
References: - A080326
Quoted from FormalConjectures/OEIS/80326.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.
OeisA80326.conjecture
Open: stated without proof.
Conjecture: \(a(n) = \text{primorial}(n)\) for infinitely many \(n\).
theorem conjecture : {n : ℕ | a n = primorial n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/80326.lean, line 75.
Sources
TheoremPrimes of the form 2^n + 2^i + 1#
There are infinite primes of the form \(2^n + 2^i + 1\), with \(0 < i < n\). See Wagstaff (2001) where this conjecture is posed.
References: - A81091 - Samuel S. Wagstaff, Jr., Prime Numbers with a fixed number of one bits or zero bits in their binary representation, Exp. Math. vol. 10, issue 2 (2001) 267.
Quoted from FormalConjectures/OEIS/81091.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.
OeisA81091.conjectureA81091
Open: stated without proof.
Conjecture (A81091): There are infinite primes of the form \(2^n + 2^i + 1\), with \(0 < i < n\).
theorem conjectureA81091 :
Set.Infinite {p : ℕ | A p}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/81091.lean, line 64.
Sources
TheoremSmallest palindrome with exactly \(n\) divisors#
The sequence \(a(n)\) is the smallest palindromic number with exactly \(n\) divisors, or \(0\) if no such number exists.
References: - A083753
Quoted from FormalConjectures/OEIS/83753.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.
OeisA83753.conjecture
Open: stated without proof.
There are no palindromic numbers greater than 1 which are the fifth or higher power of a natural number.
theorem conjecture (m k : ℕ) (hm : 1 < m) (hpal : IsDecimalPalindrome m) (hk : 5 ≤ k) :
¬ ∃ x : ℕ, m = x ^ k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/83753.lean, line 94.
Sources
TheoremSmallest prime \(p\) such that \(p + n\) is an \(n\)-th power#
Smallest prime \(p\) such that \(p + n\) is an \(n\)-th power, or \(0\) if no such number exists. That is, the smallest prime of the form \(k^n - n\).
References: - A084046
Quoted from FormalConjectures/OEIS/84046.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 4 test statements, counted here but not shown.
OeisA84046.conjecture
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-full-50usd-oai-jajpvieznaevpoyg/a084046_conjecture_0/Submission/Spec.lean#L17.
Conjecture: if a(k) = 0 then k is an even square.
This is false for \(k = 27\). Every candidate \(x^{27} - 27\) factors as \((x^9 - 3)(x^{18} + 3x^9 + 9)\), so \(a(27) = 0\), but \(27\) is not an even square.
theorem conjecture : ¬ ∀ k : ℕ, a k = 0 → ∃ m : ℕ, k = (2 * m) ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/84046.lean, line 112.
Sources
TheoremSmallest \(r\) such that (concatenation of \(n\), \(r\) times) \(\cdot 10 + 1\) is prime#
\(a(n)\) is the smallest \(r\) where (concatenation of \(n\), \(r\) times with itself) \(\cdot 10 + 1\) is a prime, or \(0\) if no such number exists. The number resulting from concatenating \(n\), \(r\) times, is \(n \cdot \sum_{i=0}^{r-1} (10^d)^i\), where \(d\) is the number of digits of \(n\).
References: - A086766
Quoted from FormalConjectures/OEIS/86766.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.
OeisA86766.conjecture1
Open: stated without proof.
What is the smallest integer \(m > 1\) such that \(a(10^m)\) is nonzero? - Farideh Firoozbakht, Jan 07 2015
theorem conjecture1 :
conjecture1.answer =
if h : ∃ m, 1 < m ∧ a (10 ^ m) ≠ 0 then
some (sInf {m | 1 < m ∧ a (10 ^ m) ≠ 0})
else
none
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/86766.lean, line 149.
OeisA86766.conjecture2
Open: stated without proof.
Conjecture: If \(n\) is not of the form \(10^m\) then \(a(n)\) is nonzero. - Farideh Firoozbakht, Jan 07 2015
theorem conjecture2 (n : ℕ) (hn : 0 < n) (h : ∀ m : ℕ, n ≠ 10 ^ m) : a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/86766.lean, line 163.
OeisA86766.conjecture3
Open: stated without proof.
What is the smallest odd prime \(p\) such that \((10^{p^2}-1)/(10^p-1)\) is a prime number (and \(a(10^{p-1})\) could be nonzero)? - Farideh Firoozbakht, Jan 07 2015
theorem conjecture3 :
conjecture3.answer =
if h : ∃ p, p.Prime ∧ 2 < p ∧ ((10 ^ (p ^ 2) - 1) / (10 ^ p - 1)).Prime then
some (sInf {p | p.Prime ∧ 2 < p ∧ ((10 ^ (p ^ 2) - 1) / (10 ^ p - 1)).Prime})
else
none
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/86766.lean, line 175.
Sources
TheoremBinary representation of primes that divide a number, in decimal#
The value \(a(n)\) is given by
\[ a(n) = \sum_{p \mid n, p \text{ prime}} 2^{\pi(p) - 1} \]where \(\pi(p) = \mathrm{primeCounting}(p)\) gives the 1-based index of the prime \(p\).
References: - A087207
Quoted from FormalConjectures/OEIS/87207.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.
OeisA87207.conjecture
Open: stated without proof.
Starting at any \(n\) and iterating the map \(n \mapsto a(n)\), we will always reach \(0\). - Antti Karttunen, Jun 18,20 2017
theorem conjecture (n : ℕ) : ∃ k : ℕ, (a^[k]) n = 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/87207.lean, line 65.
Sources
TheoremExpansion of \((1 - x)/(1 - 2 x + 3 x^2)\)#
This sequence is the expansion of \((1 - x)/(1 - 2 x + 3 x^2)\) in powers of \(x\). It satisfies the linear recurrence relation \(a(n) = 2 a(n-1) - 3 a(n-2)\) for \(n \ge 2\), with initial values \(a(0)=1\) and \(a(1)=1\).
References: - A087455
Quoted from FormalConjectures/OEIS/87455.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.
OeisA87455.conjecture
Open: stated without proof.
It is an open question whether or not this sequence satisfies Benford's law [Berger-Hill, 2017; Arno Berger, email, Jan 06 2017]. - N. J. A. Sloane, Feb 08 2017
theorem conjecture : SatisfiesBenford a
Category research open; AMS 11 Number theory, 60 Probability theory and stochastic processes. Declared in FormalConjectures/OEIS/87455.lean, line 81.
Sources
TheoremSmallest prime formed by concatenation \(n, n-1, \dots, n-k\)#
\(a(n)\) is the smallest prime which has the form of the concatenation \(n, n-1, n-2, \dots, n-k\) for some \(k < n\), or \(0\) if no such prime exists.
References: - A087571
Quoted from FormalConjectures/OEIS/87571.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.
OeisA87571.conjecture
Open: stated without proof.
Conjecture: There are infinitely many composite numbers \(n\) such that \(a(n)\) is nonzero.
theorem conjecture (M : ℕ) : ∃ n > M, 1 < n ∧ ¬ n.Prime ∧ a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/87571.lean, line 75.
Sources
TheoremConjectures associated with A087719#
Define \(\varsigma(n)\) the smallest prime factor of \(n\) (
Nat.minFac). Let \(a_n\) be the least number such that the count of numbers \(k \le a_n\) with \(k > \varsigma(k)^n\) exceeds the count of numbers with \(k \le \varsigma(k)^n\).The conjecture states that \(a_n = 3^n + 3 \cdot 2^n + 6\) for \(n \ge 1\).
References: - A087719
Quoted from FormalConjectures/OEIS/87719.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 textbook results. It also has 3 test statements, counted here but not shown.
OeisA87719.a_exists
Textbook result, stated without proof.
There exists m such that countExceeding n m > countNotExceeding n m.
theorem a_exists (n : ℕ) : ∃ m, countExceeding n m > countNotExceeding n m
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/87719.lean, line 49.
OeisA87719.a_formula
Textbook result, stated without proof. A Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/7a286754f623759d69a3dd18f482c53c1d70959b/FormalConjectures/OEIS/87719.lean#L640.
We have the following formula: \(a(n) = 3^n + 3 * 2^n + 6\) for \(n \geq 1\).
theorem a_formula {n : ℕ} (hn : n ≥ 1) : a n = 3 ^ n + 3 * 2 ^ n + 6
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/87719.lean, line 84.
Sources
TheoremNumber of pairs of twin primes between \(n^2\) and \((n+1)^2\)#
\(a(n)\) is the number of pairs of twin primes between \(n^2\) and \((n+1)^2\). This counts the number of primes \(p\) such that \(p\) and \(p+2\) are both prime, and the entire twin prime pair \((p, p+2)\) lies strictly between \(n^2\) and \((n+1)^2\). That is, \(n^2 < p\) and \(p + 2 < (n+1)^2\).
References: - A091591
Quoted from FormalConjectures/OEIS/91591.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.
OeisA91591.conjecture
Open: stated without proof.
It is conjectured that \(a(n)>0\) for all \(n>122\). Proving this would also prove Legendre's conjecture that there is a prime between \(n^2\) and \((n+1)^2\). - T. D. Noe, Feb 28 2007
theorem conjecture :
∀ n : ℕ, n > 122 → a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/91591.lean, line 65.
Sources
TheoremPrimality and primitive root property from divisibility \(n \mid (a(n-1) + 2^{n-2})\)#
\(a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)\). The sequence \(a(n)\) is composed of natural numbers, thus we define it as a function \(\mathbb{N} \to \mathbb{N}\).
References: - A091669 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/91669.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.
OeisA91669.prime_and_primitive_root_of_dvd
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/91669.wip.lean#L250.
Conjecture (for \(n > 2\)): if \(n \mid a(n-1) + 2^{n-2}\), then \(n\) is a prime with primitive root 2 (A001122). - Amiram Eldar and Thomas Ordowski, Jan 19 2020
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem prime_and_primitive_root_of_dvd (n : ℕ) (hn : n > 2) : n ∣ (a (n - 1) + 2 ^ (n - 2)) →
Nat.Prime n ∧ IsPrimitiveRoot (2 : ZMod n) (Nat.totient n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/91669.lean, line 84.
Sources
TheoremTug of war score between prime gap increases and decreases#
Score at stage \(n\) in "tug of war" between prime gap increases vs. prime gap decreases: start with score \(= 0\) at \(n = 1\) and at stage \(k > 1\), increase (resp. decrease) the score by \(1\) if the \(k\)-th prime gap is greater (resp. less) than the previous prime gap.
References: - A092243
Quoted from FormalConjectures/OEIS/92243.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 4 test statements, counted here but not shown.
OeisA92243.conjecture1
Open: stated without proof.
Is the score \(a(n) > 0\) for some \(n > 250000\)?
theorem conjecture1 : ∃ n > 250000, a n > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/92243.lean, line 88.
OeisA92243.conjecture2
Open: stated without proof.
Is the score \(a(n)\) bounded from below?
theorem conjecture2 : ∃ B : ℤ, ∀ n : ℕ, B ≤ a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/92243.lean, line 94.
OeisA92243.conjecture3
Open: stated without proof.
Is the score \(a(n)\) bounded from above?
theorem conjecture3 : ∃ B : ℤ, ∀ n : ℕ, a n ≤ B
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/92243.lean, line 100.
OeisA92243.conjecture4
Open: stated without proof.
Is the score \(a(n) > 0\) for infinitely many values of \(n\)?
theorem conjecture4 : Set.Infinite {n : ℕ | a n > 0}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/92243.lean, line 106.
OeisA92243.conjecture5
Open: stated without proof.
Is the score \(a(n) < 0\) for infinitely many values of \(n\)?
theorem conjecture5 : Set.Infinite {n : ℕ | a n < 0}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/92243.lean, line 112.
Sources
TheoremProduct of composite numbers in triangular intervals#
Product of all composite numbers between \(n(n-1)/2+1\) and \(n(n+1)/2\) (including boundaries), where \(n(n-1)/2 = \binom{n}{2}\) and \(n(n+1)/2 = \binom{n+1}{2}\).
References: - A093456
Quoted from FormalConjectures/OEIS/93456.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.
OeisA93456.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_93456_conjecture_0/Submission/Spec.lean#L109.
Conjecture: There are finitely many numbers such that \(a(n)\) is not \(\equiv 0 \pmod{a(n-1)}\). (Also mentioned in A093455.) In fact there are infinitely many such numbers.
theorem conjecture :
¬ Set.Finite {n : ℕ | 1 < n ∧ ¬ (a (n - 1) ∣ a n)}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/93456.lean, line 65.
Sources
Theorem\(\gcd(\mathrm{numerator}(H_n), n!)\)#
\(a(n) = \gcd(\mathrm{A001008}(n), n!)\), where \(\mathrm{A001008}(n)\) is the numerator of the \(n\)-th harmonic number \(H_n = \sum_{i=1}^n \frac{1}{i}\).
References: - A093818
Quoted from FormalConjectures/OEIS/93818.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.
OeisA93818.conjecture
Open: stated without proof.
Conjecture: Every odd prime occurs as a term in the sequence.
theorem conjecture (p : ℕ) (hp : p.Prime) (hp_odd : p ≠ 2) : ∃ n > 0, a n = p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/93818.lean, line 61.
Sources
TheoremRecurrence \(a(n) = (a(n-1) + a(n-2)) \pmod n\)#
\(a(0) = a(1) = 1\); \(a(n) = (a(n-1) + a(n-2)) \pmod n\).
References: - A096535
Quoted from FormalConjectures/OEIS/96535.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.
OeisA96535.conjecture
Open: stated without proof.
All numbers appear infinitely often, i.e., for every number \(k \ge 0\) and every frequency \(f > 0\) there is an index \(i\) such that \(a(i) = k\) is the \(f\)-th occurrence of \(k\) in the sequence. - Klaus Brockhaus, Aug 29 2006
theorem conjecture (k : ℕ) (N : ℕ) : ∃ i : ℕ, i > N ∧ a i = k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/96535.lean, line 64.
Sources
TheoremCoefficients in a simultaneous approximation to two polylogarithms#
Coefficients in a simultaneous approximation to \(\operatorname{Li}_2(-1)\) and \(\operatorname{Li}_3(-1)\), given by \(a(n)=\sum_{i,j=0}^{n}\binom{n}{i}^2\binom{n}{j}^2\binom{n+i}{n}\binom{i+j}{i}\).
References: - A098275 - [Li26] Wentao Li, A proof of the OEIS A098275 conjecture, 2026.
Quoted from FormalConjectures/OEIS/98275.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.
OeisA98275.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewProofs/A098275.lean#L166.
Conjecture 1: "Conjecture: \(a(n)\) is divisible by \(n+1\)." - F. Chapoton, Jan 28 2026.
Proved and formalized in Lean by Wentao Li, with AI assistance; see [Li26].
theorem conjecture_1 (n : ℕ) : n + 1 ∣ a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/98275.lean, line 66.
Sources
TheoremExpansion of g.f. \((1+x)(3+x)/(1+6x^2+x^4)\)#
This sequence is defined by the linear recurrence relation \(a(n) = -6 a(n-2) - a(n-4)\) for \(n \ge 4\), with initial values \(a(0)=3\), \(a(1)=4\), \(a(2)=-17\), \(a(3)=-24\).
References: - A100434
Quoted from FormalConjectures/OEIS/100434.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: 3 solved and 2 textbook results. It also has 5 test statements, counted here but not shown.
OeisA100434.a_even
Textbook result, proved here.
For all \(n \ge 0\), we have \(a(2n) = - c(2n+1)\).
theorem a_even (n : ℕ) : a (2 * n) = - c (2 * n + 1)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100434.lean, line 109.
OeisA100434.a_odd
Textbook result, proved here.
For all \(n \ge 0\), we have \(a(2n+1) = d(2n+1)\).
theorem a_odd (n : ℕ) : a (2 * n + 1) = d (2 * n + 1)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100434.lean, line 134.
OeisA100434.conjecture1
Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L287.
Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all \(n \ge 0\), \(c(n) + d(n) = b(n)\).
Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here \(c, d\)), and the induction step is discharged by
rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for \(n < 600\) before formalization.)
theorem conjecture1 (n : ℕ) : c n + d n = b n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100434.lean, line 166.
OeisA100434.conjecture2
Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L306.
Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all \(n \ge 0\), \(e(n) + f(n) = b(n)\).
Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here \(e, f\)), and the induction step is discharged by
rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for \(n < 600\) before formalization.)
theorem conjecture2 (n : ℕ) : e n + f n = b n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100434.lean, line 183.
OeisA100434.conjecture3
Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L335.
Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all \(n \ge 0\), \(g(n) + a(n) = b(n)\).
Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here \(g, a\)), and the induction step is discharged by
rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for \(n < 600\) before formalization.)
theorem conjecture3 (n : ℕ) : g n + a n = b n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100434.lean, line 200.
Sources
TheoremConjectures associated with A100474#
\(a(1) = 1\); \(a(n)\) is the smallest integer such that \(a(n) + a(n-1)\) has the first \(n\) distinct prime factors not used before in this construction.
References: - A100474
Quoted from FormalConjectures/OEIS/100474.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 solved. It also has 5 test statements and 9 API statements, counted here but not shown.
OeisA100474.conjecture
Open: stated without proof.
After \(a(2) = 5\), is there another prime?
theorem conjecture : ∃ n > 2, (a n).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100474.lean, line 147.
OeisA100474.next_semiprime
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a100474-next-semiprime/blob/d7781751918e63fd1268b15525bf9554c92fdd4d/lean/OeisA100474NextSemiprimeFC.lean#L1285-L1288.
What is the next semiprime in the sequence after \(a(11)\)?
theorem next_semiprime :
next_semiprime.answer =
a (sInf {n : ℕ | 11 < n ∧ (a n).IsSemiprime})
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100474.lean, line 160.
Sources
TheoremPrime-th recurrence with reversal at each step#
\[a(n) = \operatorname{reversal}(p_{a(n-1)})\]with \(a(0)=1\), where \(p_k\) is the \(k\)-th prime number.
References: - A100475
Quoted from FormalConjectures/OEIS/100475.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 solved. It also has 5 test statements and 2 API statements, counted here but not shown.
OeisA100475.conjecture_with_zero
Proved here.
If zero is admitted as a starting value, then a start other than \(1\) does go into a loop: the sequence starting at zero is constant. This records the degenerate answer created by totalizing the one-based prime recurrence at index zero.
theorem conjecture_with_zero :
∃ x : ℕ, x ≠ 1 ∧ IsUltimatelyPeriodic (aStartAt x)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100475.lean, line 113.
OeisA100475.conjecture
Open: stated without proof.
Starting at a positive value other than \(a(0) = 1\), does this sequence ever go into a loop?
The positivity hypothesis is required because the source recurrence uses the one-based prime index
p₁ = 2; thex = 0branch above is only an artifact of makingaStartAttotal onℕ.
theorem conjecture :
∃ x : ℕ, 0 < x ∧ x ≠ 1 ∧ IsUltimatelyPeriodic (aStartAt x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/100475.lean, line 126.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.