Riesel Problem to Number of refactorable numbers…

TheoremRiesel Problem#

Riesel problem: let \(k=2n-1\); then \(a(n)\) is the smallest \(m \ge 1\) such that \(k \cdot 2^m-1\) is prime, or \(-1\) if no such prime exists.

References: - A108129

Quoted from FormalConjectures/OEIS/108129.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 and 1 API statement, counted here but not shown.

OeisA108129.conjecture

Open: stated without proof.

It is conjectured that the integer \(k = 509203\) is the smallest Riesel number, that is, the first \(n\) such that \(a(n) = -1\) is \(254602\).

theorem conjecture :
    a 254602 = -1 ∧ (∀ n : ℕ, 1 ≤ n ∧ n < 254602 → a n ≠ -1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108129.lean, line 73.

Sources
LeanOeisA108129.conjecture

Theorem\(a(n) = 16n^2 + 1\)#

References: - A108211

Quoted from FormalConjectures/OEIS/108211.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.

OeisA108211.conjecture

Solved: stated here; a Lean proof is at https://github.com/chy4pro/formal-conjectures/blob/f24f80aeaa3d5073bf4a54ed9daa102a5e0f1fad/FormalConjectures/OEIS/108211.lean#L540.

Conjecture:

\[a(n) = \left\lfloor \frac{1}{\frac{1}{4n} - \log(2) + \frac{1}{n+1} + \frac{1}{n+2} + \dots + \frac{1}{2n}} \right\rfloor.\]

Proof sketch (certificate style; the kernel-checked development lives at the formal_proof permalink below). Write \(T(n) = \log 2 - (H(2n) - H(n))\) for the harmonic tail defect. The proof sandwiches \(T(n)\) between two explicit telescoping bounds — \(h(n)\) from below and \(h(n) + 60/(4n+1)^7\) from above, where \(h\) telescopes a degree-7 rational certificate. The two resulting inequalities reduce to polynomial coefficient-nonnegativity facts discharged by elementary tactics, after which the reciprocal lands in \([16n^2 + 1,\, 16n^2 + 2)\) and the floor evaluates exactly.

theorem conjecture (n : ℕ) (hn : n > 0) :
    (a n : ℝ) =
      (⌊ 1 / ((4 * n : ℝ)⁻¹ - log 2 + ∑ k ∈ (Finset.Icc (n + 1) (2 * n)), (k : ℝ)⁻¹) ⌋ : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108211.lean, line 71.

Sources
LeanOeisA108211.conjecture

TheoremDigital sum of the Fermat number \(2^{2^n} + 1\)#

a n is the digital sum of the Fermat number \(2^{2^n} + 1\). The conjecture asks if there are any prime numbers in this sequence beyond \(n=11\).

References: - A108301

Quoted from FormalConjectures/OEIS/108301.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 5 test statements, counted here but not shown.

OeisA108301.primes_in_a

Textbook result, proved here.

\(a(0)\), \(a(1)\), \(a(5)\), \(a(6)\), \(a(7)\) and \(a(11)\) are primes.

theorem primes_in_a :
    (a 0).Prime ∧ (a 1).Prime ∧ (a 5).Prime ∧
    (a 6).Prime ∧ (a 7).Prime ∧ (a 11).Prime

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108301.lean, line 58.

OeisA108301.conjecture

Open: stated without proof.

\(a(0)\), \(a(1)\), \(a(5)\), \(a(6)\), \(a(7)\) and \(a(11)\) are primes. Are there any more?

theorem conjecture : ∃ n > 11, (a n).Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108301.lean, line 67.

Sources
LeanOeisA108301.primes_in_a · OeisA108301.conjecture

TheoremA108306: Expansion of \((3x+1)/(1-3x-3x^2)\)#

This sequence satisfies the linear recurrence relation \(a(0)=1\), \(a(1)=6\), and \(a(n) = 3a(n-1) + 3a(n-2)\) for \(n \ge 2\).

References: - A108306

Quoted from FormalConjectures/OEIS/108306.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 5 test statements, counted here but not shown.

OeisA108306.a_is_invert_transform_case

Textbook result, proved here.

The sequence is the INVERT transform of (1, 5, 10, 20, 40, 80, 160, ...) and can be obtained by extracting the upper left terms of matrix powers of [(1,5); (1,2)]. These results are a case (a=5, b=2) of the general conjecture below.

theorem a_is_invert_transform_case (n : ℕ) :
    a n = (m ^ (n + 1)) 0 0

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108306.lean, line 76.

OeisA108306.conjecture

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-108306/blob/2e01e81b20a56880993e174ee4af0f0d7af37bdd/lean/OeisA108306FC.lean#L101-L106.

The conjecture: The INVERT transform of a sequence starting \((1, a, ab, ab^2, ab^3, \ldots)\) is equivalent to extracting the upper left terms of powers of the 2x2 matrix [(1,a); (1,b)].

theorem conjecture (a_val b_val n : ℕ) :
    invertSeqD a_val b_val n = (genMatrix a_val b_val ^ n) 0 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108306.lean, line 123.

Sources
LeanOeisA108306.a_is_invert_transform_case · OeisA108306.conjecture

TheoremNumbers \(n\) such that \(\phi(n) = \phi(n + \phi(n))\)#

References: - A108569

Quoted from FormalConjectures/OEIS/108569.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.

OeisA108569.conjecture

Open: stated without proof.

Conjecture: Except for the first term all terms are even.

theorem conjecture : ∀ n, 0 < n → Even (a n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108569.lean, line 85.

Sources
LeanOeisA108569.conjecture

TheoremNumbers \(n\) such that the perfect deficiency of \(n\) is \(\le 10\).#

The perfect deficiency of \(n\) (A109883) is the remainder after greedily subtracting from \(n\) its divisors in increasing order, skipping any divisor larger than the current remainder.

References: - A108864 - A109883

Quoted from FormalConjectures/OEIS/108864.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.

OeisA108864.conjecture

Open: stated without proof.

Is \(1155\) the last odd number in this sequence? (\(1155\) is the \(59\)th term starting from \(1\), corresponding to \(a(58) = 1155\)).

theorem conjecture :
    ∀ n > 58, Even (a n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108864.lean, line 105.

Sources
LeanOeisA108864.conjecture

TheoremNumerator of \(\sum_{k=1}^n 2^k/k\).#

Conjecture: for \(n > 3\), \(\textrm{numerator}(-2/n + \sum_{k=1}^{n} \frac{2^k}{k}) == 0 (\textrm{mod} n^2)\) if and only if n is prime.

References: - A108866

Quoted from FormalConjectures/OEIS/108866.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.

OeisA108866.conjecture

Open: stated without proof.

Conjecture: for \(n > 3\), \(\textrm{numerator}(-2/n + \sum_{k=1}^{n} \frac{2^k}{k}) == 0 (\textrm{mod} n^2)\) if and only if n is prime.

theorem conjecture {n : ℕ} (hn : n > 3) :
    (ratExpression n).num ≡ 0 [ZMOD (n^2 : ℤ)] ↔ n.Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/108866.lean, line 76.

Sources
LeanOeisA108866.conjecture

TheoremNumerator of \(\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right)\)#

The sequence \(a(n)\) is the numerator of \(\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right)\). The OEIS entry records the conjecture that this ratio equals \(\text{A005156}(n) / \text{A005156}(n-1)\), where \(\text{A005156}(n)\) is the number of \((2n+1) \times (2n+1)\) vertically symmetric alternating sign matrices (VSASMs). This follows from Robbins's VSASM product formula, proved by Kuperberg (2002).

References: - A109074 - A005156 - G. Kuperberg, "Symmetry classes of alternating-sign matrices under one roof," arXiv:math/0008184, Ann. of Math. 156 (2002), 835–866.

Quoted from FormalConjectures/OEIS/109074.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 10 test statements, counted here but not shown.

OeisA109074.conjecture

Solved: stated here without proof.

"It is conjectured that \(\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right) = \text{A005156}(n+1)/\text{A005156}(n)\)."

The OEIS comment indexes A005156 from \(1\); for the \(0\)-indexed sequence b this states frac (n + 1) = b (n + 1) / b n. This holds by the product formula

\[\text{A005156}(n) = \frac{1}{2^n} \prod_{k=1}^{n} \frac{(6k-2)!\,(2k-1)!}{(4k-1)!\,(4k-2)!}\]

conjectured by Robbins and proved by Kuperberg (2002).

theorem conjecture (n : ℕ) :
    frac (n + 1) = (b (n + 1) : ℚ) / (b n : ℚ)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/OEIS/109074.lean, line 153.

Sources
LeanOeisA109074.conjecture

TheoremConjectures associated with A109227#

Binary strings that have 1's where primes occur, 0's elsewhere and every term ends with the \(n\)-th prime index.

Conjecture: \(a(2)\) and \(a(121)\) are primes. Are there any more?

References: - A109227

Quoted from FormalConjectures/OEIS/109227.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.

OeisA109227.conjecture

Open: stated without proof.

Conjecture: \(a(2)\) and \(a(121)\) are primes. Are there any more?

theorem conjecture :
    ∃ n > 0, n ≠ 2 ∧ n ≠ 121 ∧ (a n).Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109227.lean, line 85.

Sources
LeanOeisA109227.conjecture

TheoremConjectures associated with A109671#

\(a(1)=1\); thereafter, \(a(2n)=a(n)\), \(a(2n+1)\) is the smallest positive number such that \(|a(2n+1)-a(2n-1)|=a(n)\). Conjecture: Does the sequence contain every positive integer?

References: - A109671

Quoted from FormalConjectures/OEIS/109671.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.

OeisA109671.conjecture

Open: stated without proof.

Does the sequence contain every positive integer (cf. A169741)?

theorem conjecture :
    ∀ m : ℕ, 0 < m → ∃ n : ℕ, 0 < n ∧ a n = m

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109671.lean, line 74.

Sources
LeanOeisA109671.conjecture

TheoremConjectures associated with A109845#

\(a(1) = 2\); \(a(2n)\) = lcm of all previous terms + 1; \(a(2n+1)\) = lcm of all previous terms - 1.

References: - A109845

Quoted from FormalConjectures/OEIS/109845.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.

OeisA109845.conjecture

Open: stated without proof.

Conjecture: There are infinitely many primes in this sequence.

theorem conjecture : Set.Infinite {n : ℕ | (a n).Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109845.lean, line 69.

Sources
LeanOeisA109845.conjecture

TheoremConjectures associated with A109905#

\(a(n)\) is the greatest prime of the form \(k(n-k)+1\), where \(k\) can take values from \(1\) to \(\lfloor n/2 \rfloor\). \(a(n)=0\) if no such prime exists.

References: - A109905

Quoted from FormalConjectures/OEIS/109905.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.

OeisA109905.conjecture

Open: stated without proof.

\(a(n) = 0\) for \(n = 1\), \(6\), \(30\) and \(54\). Are there any others?

theorem conjecture :
    ∃ n : ℕ, n > 0 ∧ a n = 0 ∧ n ∉ ({1, 6, 30, 54} : Finset ℕ)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109905.lean, line 64.

Sources
LeanOeisA109905.conjecture

TheoremConjectures associated with A109908#

\(a(n)\) = greatest prime of the form \(k(n-k)-1\), or \(0\) if no such prime exists.

References: - A109908

Quoted from FormalConjectures/OEIS/109908.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.

OeisA109908.conjecture

Open: stated without proof.

Conjecture: \(a(n) > 0\) for \(n > 3\).

theorem conjecture : ∀ n > 3, a n > 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109908.lean, line 61.

Sources
LeanOeisA109908.conjecture

TheoremConjectures associated with A109909#

\(a(n)\) = number of primes of the form \(k(n-k)-1\).

References: - A109909

Quoted from FormalConjectures/OEIS/109909.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.

OeisA109909.conjecture

Open: stated without proof.

Conjecture: \(a(n) > 0\) for \(n > 3\).

theorem conjecture : ∀ n > 3, a n > 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/109909.lean, line 61.

Sources
LeanOeisA109909.conjecture

TheoremNumber of symbols '*' and '^' to write the canonical prime factorization of n#

The canonical prime factorization is \(n = p_1^{e_1} p_2^{e_2} \cdots p_k^{e_k}\). The written form is \(p_1^{\wedge} e_1 * p_2^{\wedge} e_2 * \cdots * p_k^{\wedge} e_k\), where the \(\wedge\) appears only if \(e_i > 1\). \(a(n) = (\text{number of distinct prime factors}) - 1 +\) \((\text{number of distinct prime factors with exponent } > 1)\).

References: - A110475

Quoted from FormalConjectures/OEIS/110475.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.

OeisA110475.conjecture

Open: stated without proof.

It is conjectured that \(1,2,3,4,5,6,7,9,11\) are the only positive integers which cannot be represented as the sum of two elements of indices \(n\) such that \(a(n) = 1\).

theorem conjecture :
  ∀ m > 0, m ∉ exceptionalSet ↔ ∃ x y : ℕ, a x = 1 ∧ a y = 1 ∧ m = x + y

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/110475.lean, line 94.

Sources
LeanOeisA110475.conjecture

Theorem\(a(n) = \operatorname{lcm}\{1,2,\dots,n\}/\operatorname{denom}(H(n))\)#

References: - A110566

Quoted from FormalConjectures/OEIS/110566.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.

OeisA110566.conjecture

Open: stated without proof.

It is conjectured that every odd number occurs in this sequence.

theorem conjecture :
  ∀ m : ℕ, Odd m → ∃ n > 0, a n = m

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/110566.lean, line 78.

Sources
LeanOeisA110566.conjecture

TheoremSmallest \(m > 0\) such that there are no primes between \(nm\) and \(n(m+1)\) inclusive.#

Sierpinski's conjecture (1958) is precisely that a(n) >= n for all n.

References: - A110835

Quoted from FormalConjectures/OEIS/110835.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.

OeisA110835.conjecture

Open: stated without proof.

Sierpinski's conjecture (1958) is precisely that \(a(n) >= n\) for all \(n\).

theorem conjecture : ∀ n > 0, a n ≥ n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/110835.lean, line 111.

Sources
LeanOeisA110835.conjecture

TheoremConjectures associated with A110854#

\(a(n) = \mathrm{prime}(2n+2) - \mathrm{prime}(2n+1) - \mathrm{prime}(2n) + \mathrm{prime}(2n-1)\), where \(\mathrm{prime}(k)\) is the \(k\)-th prime number.

References: - A110854

Quoted from FormalConjectures/OEIS/110854.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 and 5 API statements, counted here but not shown.

OeisA110854.conjecture

Open: stated without proof.

Do the absolute values cover A004275? A004275 is \(1\) together with the nonnegative even numbers. The conjecture asks whether every member of A004275 occurs as \(|a(n)|\) for some term of the sequence.

theorem conjecture :
  ∀ d : ℕ, (d = 1 ∨ Even d) → ∃ n > 0, d = (a n).natAbs

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/110854.lean, line 106.

Sources
LeanOeisA110854.conjecture

TheoremInteger part of \(\mathrm{prime}(n)/\pi(n)\)#

Here \(\mathrm{prime}(n)\) is the \(n\)-th prime number, and \(\pi(n)\) is the prime-counting function.

References: - A111114

Quoted from FormalConjectures/OEIS/111114.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.

OeisA111114.conjecture

Open: stated without proof.

Conjecture: As \(n \rightarrow \infty\), there are infinitely many n's such that \(a(n)\) is greater than \(a(n+1)\).

theorem conjecture : ∃ᶠ n in atTop, a n > a (n + 1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/111114.lean, line 78.

Sources
LeanOeisA111114.conjecture

TheoremNumber of refactorable numbers (A033950) \(\le 10^n\)#

A number \(k\) is refactorable if its number of divisors, \(\tau(k)\), divides \(k\).

References: - A111291 - [Co99] Colton, S., Refactorable numbers - a machine invention. J. Integer Seq. 2 (1999), Article 99.1.2. - [Ze02] Zelinsky, J., Tau numbers: a partial proof of a conjecture and other results. J. Integer Seq. 5 (2002), Article 02.2.8. - [Sp85] Spiro, C., How often is the number of divisors of n a divisor of n? J. Number Theory 21 (1985), 81--100.

Quoted from FormalConjectures/OEIS/111291.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 6 test statements, counted here but not shown.

OeisA111291.conjecture

Solved: stated here without proof.

Simon Colton conjectures that the number of refactorable numbers less than \(x\) is at least \(\frac{x}{2\log x}\). This is an asymptotic claim, so we state it for sufficiently large \(x\).

In this form it is a theorem: Zelinsky [Ze02, Theorem 7] proved that for every \(k\) the number of refactorable numbers \(\le n\) exceeds \(k \pi(n)\) for all sufficiently large \(n\), and \(\pi(n) \sim n / \log n\). It also follows from Spiro's asymptotic [Sp85], by which the count is \(\frac{x}{\sqrt{\log x}} (\log \log x)^{-1 + o(1)}\). See colton_conjecture for the pointwise conjecture that remains open.

theorem conjecture : ∀ᶠ x in Filter.atTop,
    (countRefactorable x : ℝ) ≥ x / (2 * Real.log x)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/111291.lean, line 88.

OeisA111291.colton_conjecture

Open: stated without proof.

Colton's conjecture [Co99] as stated by Zelinsky [Ze02]: for every \(n\), the number of refactorable numbers \(\le n\) is at least half the number of primes \(\le n\), i.e. \(\pi(n) \le 2\,T(n)\).

Zelinsky [Ze02] proved this for all sufficiently large \(n\) (see conjecture), with an explicit bound of \(7.42 \cdot 10^{13}\) beyond which it holds; the remaining range is open.

theorem colton_conjecture : ∀ n : ℕ, Nat.primeCounting n ≤ 2 * countRefactorableNat n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/111291.lean, line 101.

Sources
LeanOeisA111291.conjecture · OeisA111291.colton_conjecture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.