Conjectures associated with… to Decimal encoding of the prime…

TheoremConjectures associated with A038552#

A038552 lists the largest squarefree number \(k\) such that the imaginary quadratic field \(\mathbb{Q}(\sqrt{-k})\) has class number \(n\).

The conjectures state that: 1. All terms are congruent to \(19 \pmod{24}\). 2. This is also the largest absolute value of negative fundamental discriminant \(d\) for class number \(n\). 3. For even \(n\), if \(k\) is the largest odd number with \(h(-k) = n\) and \(k'\) is the largest even number with \(h(-k') = n\), then \(k > k'\). Here \(h(D)\) is the class number of the quadratic field with discriminant \(D\), so \(k\) and \(k'\) are absolute values of negative fundamental discriminants, not radicands. The source states conjecture 2 in this form.

The squarefree condition in the definition is needed for the maximum to exist, since \(\mathbb{Q}(\sqrt{-k}) = \mathbb{Q}(\sqrt{-4k})\).

Conjecture 2 is not a restatement of the definition. Both maxima range over the same imaginary quadratic fields, but they maximize different integers attached to those fields. A038552 uses the squarefree radicand \(k\), whereas the discriminant of \(\mathbb{Q}(\sqrt{-k})\) is \(-k\) for \(k \equiv 3 \pmod 4\) and \(-4k\) otherwise. The map \(k \mapsto |d|\) is not monotone: it sends \(2\) to \(8\) and \(3\) to \(3\). So conjecture 2 says that the largest term \(k\) satisfies \(k \equiv 3 \pmod 4\), and that \(4k' \le k\) for every \(k' \equiv 1, 2 \pmod 4\) with class number \(n\).

References: - [Sta67] Stark, Harold M. "A complete determination of the complex quadratic fields of class-number one." Michigan Mathematical Journal 14.1 (1967): 1-27. - oeis.org/A038552

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

OeisA38552.starkHeegner_classNumberOne

Solved: stated here without proof.

The Stark-Heegner theorem [Sta67] implies that the squarefree \(k > 0\) such that \(\mathbb{Q}(\sqrt{-k})\) has class number \(1\) are exactly \(\{1, 2, 3, 7, 11, 19, 43, 67, 163\}\).

theorem starkHeegner_classNumberOne :
    {k : ℕ | Squarefree k ∧ HasClassNumber k 1} = {1, 2, 3, 7, 11, 19, 43, 67, 163}

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

OeisA38552.mod_24_of_isA038552

Open: stated without proof.

All terms of A038552 are congruent to \(19 \pmod{24}\).

theorem mod_24_of_isA038552 {n k : ℕ} (h : IsA038552 n k) : k % 24 = 19

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

OeisA38552.isA038552_eq_largestNegFundDisc

Open: stated without proof.

A038552 also gives the largest absolute value of negative fundamental discriminant for each class number.

theorem isA038552_eq_largestNegFundDisc {n k : ℕ} (h : IsA038552 n k) :
    IsLargestNegFundDiscrForClassNumber (n := n) k

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

OeisA38552.largestEven_lt_largestOdd_negFundDisc

Open: stated without proof.

For even class number \(n\), let \(k\) be the largest odd number such that the quadratic field with discriminant \(-k\) has class number \(n\), and let \(k'\) be the largest even such number, when they exist. Then \(k > k'\).

theorem largestEven_lt_largestOdd_negFundDisc {n k k' : ℕ} (hn : Even n)
    (hk : IsGreatest {m : ℕ | Odd m ∧ IsFundamentalDiscr (-m : ℤ) ∧
      classNumberOfDiscriminant (-m : ℤ) = n} k)
    (hk' : IsGreatest {m : ℕ | Even m ∧ IsFundamentalDiscr (-m : ℤ) ∧
      classNumberOfDiscriminant (-m : ℤ) = n} k') : k' < k

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

Sources
LeanOeisA38552.starkHeegner_classNumberOne · OeisA38552.mod_24_of_isA038552 · OeisA38552.isA038552_eq_largestNegFundDisc · OeisA38552.largestEven_lt_largestOdd_negFundDisc

TheoremSmallest composite \(c\) such that \(\textrm{primorial}(n) + c\) is prime#

References: - A038771

Quoted from FormalConjectures/OEIS/38771.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: 2 open and 1 textbook result. It also has 4 test statements, counted here but not shown.

OeisA38771.a_n_exists

Textbook result, proved here.

\(a(n) \ne 0\) for all \(n\) (i.e., a suitable composite \(c\) always exists). The following more general statement follows from Dirichlet's theorem on primes in arithmetic progressions: there doesn't exist a > 0 natural number such that p - a is prime for every prime p > a.

Choose q prime such that q is coprime with a, and p > a + q prime such that q | p - a (such a p exists from Dirichlet's theorem). Then p - a is composite, a contradiction.

theorem a_n_exists (n : ℕ) : a n ≠ 0

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

OeisA38771.conjecture1

Open: stated without proof.

Conjecture: \(\liminf_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 1 <\) \(\limsup_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 2\). - Charles R Greathouse IV and Thomas Ordowski, Apr 24 2015

theorem conjecture1 :
    let p_next_sq (n : ℕ) : ℝ := ((Nat.nth Nat.Prime n : ℝ)) ^ 2
    let seq (n : ℕ) : ℝ := (a n : ℝ) / p_next_sq n
    (liminf seq atTop = 1) ∧ (limsup seq atTop = 2)

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

OeisA38771.conjecture2

Open: stated without proof.

All the terms in this sequence have exactly two prime factors. This conjecture is true for the first 133 terms. - Dmitry Kamenetsky, Jan 06 2019

theorem conjecture2 (n : ℕ) : (a n).IsSemiprime

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

Sources
LeanOeisA38771.a_n_exists · OeisA38771.conjecture1 · OeisA38771.conjecture2

TheoremDenominators of coefficients in Stirling's expansion for \(\log(\Gamma(z))\)#

The \(n\)-th term is the denominator of \(\frac{B_{2n}}{2n(2n-1)}\) where \(B_{2n}\) is the \(2n\)-th Bernoulli number.

References: - A046969

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

OeisA46969.conjecture1

Open: stated without proof.

Conjecture I: if \(n > 2\), then \(\frac{a(\text{A005382}(n))}{12}\) is prime, where A005382 is the sequence of primes \(p\) such that \(2p-1\) is also prime. Since \(\text{A005382}(1) = 2\), \(\text{A005382}(2) = 3\) and \(\text{A005382}(3) = 7\), this says that \(\frac{a(p)}{12}\) is prime for every prime \(p > 3\) such that \(2p-1\) is also prime. - Lorenzo Sauras Altuzarra, Oct 13 2020

theorem conjecture1 (p : ℕ) (hp : p.Prime) (hp' : (2 * p - 1).Prime) (h3 : 3 < p) :
    (a p / 12).Prime

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

OeisA46969.conjecture2

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-full-50usd-ant-j0j0g4uzligm1k41/oeis_a046969_conjecture_2/Submission/Spec.lean#L845.

Conjecture II: if \(\frac{a(n)}{12}\) is prime, then \(\frac{a(n-1)}{12} - (n-1)\), \(\frac{a(n)}{12} - n\) and \(\frac{a(n+2)}{12} - (n+2)\) are multiples of 6. - Lorenzo Sauras Altuzarra, Oct 13 2020

This is false for \(n = 236791\).

theorem conjecture2 :
    ¬ ∀ (n : ℕ), 2 ≤ n → 12 ∣ a n → Nat.Prime (a n / 12) →
      12 ∣ a (n - 1) → 12 ∣ a (n + 2) →
      6 ∣ ((a (n - 1) / 12 : ℤ) - (n - 1 : ℤ)) ∧
      6 ∣ ((a n / 12 : ℤ) - (n : ℤ)) ∧
      6 ∣ ((a (n + 2) / 12 : ℤ) - (n + 2 : ℤ))

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

Sources
LeanOeisA46969.conjecture1 · OeisA46969.conjecture2

Theorem\(a(n) = \sum_{k=1}^n (k^2 \bmod n)\)#

References: - A048153

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

OeisA48153.conjecture

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-lite-200usd-ant-me0xxoowyqauyrvj/oeis_48153_conjecture_0/Submission/Spec.lean#L3215.

"Conjecture: \(a(n) <= \frac{n^2-1}{2}\). - Aspen A.M. Meissner, Mar 06 2025"

theorem conjecture (n : ℕ) (hn : 1 ≤ n) : a n ≤ (n ^ 2 - 1) / 2

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

Sources
LeanOeisA48153.conjecture

TheoremNearest integer to \(n/\sqrt{2}\)#

Nearest integer to \(n/\sqrt{2}\), defined by \(\lfloor n/\sqrt{2} + 1/2 \rfloor\).

References: - A049473

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

OeisA49473.conjecture

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a049473-zeta3-beatty/blob/b3a74bf/lean/OeisA49473FC.lean#L667-L673.

Let \(s(n) = \zeta(3) - \sum_{k=1}^n \frac{1}{k^3}\). Conjecture: for \(n \ge 1\), \(s(a(n)) < \frac{1}{n^2} < s(a(n)-1)\), and the difference sequence of A049473 consists solely of \(0\)'s and \(1\)'s, in positions given by the nonhomogeneous Beatty sequences A001954 and A001953, respectively. - Clark Kimberling, Oct 05 2014

theorem conjecture :
    (∀ n : ℕ, 1 ≤ n → s (a n) < 1 / (n : ℝ) ^ 2 ∧ 1 / (n : ℝ) ^ 2 < s (a n - 1)) ∧
    (∀ n : ℕ, 1 ≤ n →
      let diff : ℕ := a n - a (n - 1)
      (diff = 0 ↔ n - 1 ∈ A001954) ∧ (diff = 1 ↔ n - 1 ∈ A001953))

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

Sources
LeanOeisA49473.conjecture

TheoremAsymptotics of subsets of \(\{1, 2, \dots, n\}\) with integer average#

Number of nonempty subsets of \(\{1, 2, 3, \dots, n\}\) whose elements have an integer average.

Benoit Cloitre conjectured the asymptotic expansion:

\[a(n) = \frac{2^{n+1}}{n} \left(1 + \frac{1}{n} + \frac{3}{n^2} + \frac{13}{n^3} + \frac{75}{n^4} + \frac{541}{n^5} + o\left(\frac{1}{n^5}\right)\right)\]

where the coefficients \(1, 1, 3, 13, 75, 541, \dots\) are the Fubini numbers (preferential arrangements, A000670).

References: - A051293 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - A000670

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

OeisA51293.tendsto_aReal_asymptotic

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/51293.wip.lean#L503.

Conjecture: \(a(n) = 2^{n+1}/n \cdot (1 + 1/n + 3/n^2 + 13/n^3 + 75/n^4 + 541/n^5 + o(1/n^5))\). - Benoit Cloitre, Oct 20 2002

A formal proof has been found with the methods described in arxiv/2605.22763.

theorem tendsto_aReal_asymptotic :
    Tendsto (fun n : ℕ =>
      (aReal n - (2 ^ (n + 1) / (n : ℝ)) *
        (1 + 1 / (n : ℝ) + 3 / (n : ℝ) ^ 2 + 13 / (n : ℝ) ^ 3 + 75 / (n : ℝ) ^ 4 + 541 / (n : ℝ) ^ 5)) /
      (2 ^ (n + 1) / (n : ℝ) ^ 6)) atTop (nhds 0)

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

Sources
LeanOeisA51293.tendsto_aReal_asymptotic

TheoremMaximum exponent in the prime factorization of \(n\)#

References: - A051903

Quoted from FormalConjectures/OEIS/51903.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved. It also has 5 test statements, counted here but not shown.

OeisA51903.conjecture1

Open: stated without proof.

Are there composite numbers \(n > 4\) such that \(n \equiv a(n) \pmod{\phi(n)}\)? - Thomas Ordowski, Dec 02 2019

This question is equivalent to Lehmer's totient problem LehmerTotient.lehmer_totient; a positive answer here falsifies the universal statement asked about in Erdos828.erdos_828.variants.lehmer_conjecture. Any composite \(n\) with \(\phi(n) \mid n - 1\) is squarefree, so \(a(n) = 1\) and the condition here holds. Conversely, let \(n > 4\) be composite with \(\phi(n) \mid n - a(n)\) and \(e = a(n) \ge 2\), and pick \(p\) with \(p^e \mid n\). Then \(p^{e-1} \mid \phi(n) \mid n - e\) and \(p^{e-1} \mid n\), so \(p^{e-1} \mid e\), which forces \(p = 2\) and \(e = 2\). Now \(n = 4m\) with \(m\) odd and squarefree, and \(2\phi(m) \mid 4m - 2\) makes \(\phi(m)\) odd, so \(m = 1\) and \(n = 4\). Hence \(e = 1\) and the condition is \(\phi(n) \mid n - 1\).

theorem conjecture1 :
    ∃ n : ℕ, 4 < n ∧ ¬ n.Prime ∧ n.totient ∣ (n - a n)

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

OeisA51903.conjecture2

Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A051903/blob/c0104e7a9cc2d76d86c3a277c372f91a9553a0f6/lean/DMSolutions/OEIS_A051903/Solution.lean#L21-L24.

Are there odd numbers \(n\) such that \(a(n) > 1\) and \(n \equiv a(n) \pmod{\lambda(n)}\)? (Equivalently, odd numbers \(n\) such that \(a(n) > 1\) and \(b^n \equiv b^{a(n)} \pmod n\) for all \(b\).) - Thomas Ordowski, Dec 02 2019

The answer is no. Let \(q^E \| n\) with \(E = a(n) \ge 2\) and take \(b = q + 1\): then \((q+1)^{n-E} \equiv 1 \pmod{q^E}\), so lifting the exponent gives \(q^{E-1} \mid n - E\). Since also \(q^{E-1} \mid n\), we get \(q^{E-1} \mid E\), which is impossible for \(q \ge 3\).

theorem conjecture2 :
    ¬ ∃ n : ℕ, Odd n ∧ 1 < a n ∧ ∀ b : ℕ, b ^ n ≡ b ^ (a n) [MOD n]

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

OeisA51903.conjecture3

Solved: stated here; a Lean proof is at https://github.com/anshM123/OEIS-A051903/blob/c0104e7a9cc2d76d86c3a277c372f91a9553a0f6/lean/DMSolutions/OEIS_A051903/Solution.lean#L27-L30.

Are there odd numbers \(n\) such that \(a(n) > 1\) and \(n \equiv a(n) \pmod{\operatorname{ord}_n(2)}\)? (Equivalently, odd numbers \(n\) such that \(a(n) > 1\) and \(2^n \equiv 2^{a(n)} \pmod n\).) - Thomas Ordowski, Dec 02 2019

The answer is yes: \(n = 7 \cdot 631 \cdot 881 \cdot 3511^2 \cdot 201961 = 9687963167864344937\) is odd, \(a(n) = 2\) and \(2^n \equiv 2^2 \pmod n\). A square factor \(q^2 \mid n\) forces \(q\) to be a Wieferich prime; \(3511\) works because \(\operatorname{ord}_{3511^2}(2) = 1755\) is odd and \(n \equiv 2 \pmod{1755}\).

theorem conjecture3 :
    ∃ n : ℕ, Odd n ∧ 1 < a n ∧ 2 ^ n ≡ 2 ^ (a n) [MOD n]

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

Sources
LeanOeisA51903.conjecture1 · OeisA51903.conjecture2 · OeisA51903.conjecture3

TheoremExpansion of g.f. \((1-\sqrt{1-4x-4x^2})/(2(1+x))\)#

The \(n\)-th term \(a(n)\) is given by

\[a(n) = \sum_{k=0}^{n-1} \frac{1}{k+1} \binom{2k}{k} \binom{k}{n-1-k}\]

References: - A052709

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

OeisA52709.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_52709_conjecture_0/Submission/Spec.lean#L1289.

Conjecture: for \(n > 0\), \(a(n)\) is also the number of sequences of length \(n - 1\) covering an initial interval of positive integers and avoiding three terms \((\dots, x, \dots, y, \dots, z, \dots)\) such that \(x \le y \le z\). - Gus Wiseman, Jun 17 2021

theorem conjecture (n : ℕ) (hn : 0 < n) [Fintype (sequencesCountedByA052709 n)] :
    a n = Fintype.card (sequencesCountedByA052709 n)

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

Sources
LeanOeisA52709.conjecture

Theorem\(a(n) = (\text{smallest prime} > n^2) - n^2\)#

The difference between the smallest prime strictly greater than \(n^2\) and \(n^2\).

References: - A053000

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

OeisA53000.conjecture

Open: stated without proof.

Conjecture: \(a(n) \le 1 + \phi(n)\) for \(n > 0\). This improves on Oppermann's conjecture, which says \(a(n) < n\). - Thomas Ordowski, Dec 17 2014

theorem conjecture (n : ℕ) (hn : 0 < n) : a n ≤ 1 + n.totient

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

Sources
LeanOeisA53000.conjecture

TheoremConcatenation of the next \(n\) numbers#

\(a(n)\) is the concatenation of the next \(n\) numbers: the integers from \(\frac{(n-1)n}{2} + 1\) up to \(\frac{n(n+1)}{2}\).

References: - A053067

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

OeisA53067.conjecture

Open: stated without proof.

"The second term is a prime. When is the next prime, if there is another? - N. J. A. Sloane, Dec 16 2016"

theorem conjecture :
    conjecture.answer =
      if h : ∃ n, 2 < n ∧ (a n).Prime then
        some (sInf {n | 2 < n ∧ (a n).Prime})
      else
        none

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

Sources
LeanOeisA53067.conjecture

TheoremCatalan-Larcombe-French sequence#

The Catalan-Larcombe-French sequence defined by \(a(0)=1\), \(a(1)=8\), and

\[n^2 a(n) = 8(3n^2 - 3n + 1) a(n-1) - 128(n-1)^2 a(n-2)\]

for \(n \ge 2\).

References: - A053175 - [ZS18] Zhu, B.-X., Sun, Z.-W., Hankel-type determinants for some combinatorial sequences, Int. J. Number Theory 14 (2018), 1265-1277

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

OeisA53175.conjecture

Solved: stated here without proof.

Conjecture: let \(P(n)\) be the \((n+1) \times (n+1)\) Hankel-type determinant with \((i,j)\)-entry equal to \(a(i+j)\) for all \(i,j = 0, \ldots, n\). Then \(P(n)/2^{n(n+3)}\) is a positive odd integer. - Zhi-Wei Sun, Aug 14 2013

Proved by [ZS18], Theorem 1.2: \(2^{-n(n+3)} |P_{i+j}|_{0 \le i,j \le n}\) is a positive odd integer for every \(n \in \mathbb{N}\), where \(P_n\) are the Catalan-Larcombe-French numbers.

theorem conjecture (n : ℕ) :
    let detP := (hankelMatrix n).det
    let pow2 := (2 : ℤ) ^ (n * (n + 3))
    pow2 ∣ detP ∧ 0 < detP / pow2 ∧ (detP / pow2) % 2 = 1

Category research solved; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/53175.lean, line 84.

Sources
LeanOeisA53175.conjecture

TheoremLeast \(m\) such that \(\phi(m) = n!\)#

The smallest positive integer \(m\) whose Euler totient equals \(n!\).

References: - A055487

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

OeisA55487.conjecture

Open: stated without proof.

Conjecture: unless \(n! + 1\) is prime (i.e., \(n \in \text{A002981}\)), \(a(n) = p q\) where \(p\) is the least prime \(> \sqrt{n!}\) such that \((p - 1) \mid n!\) and \(q = \frac{n!}{p - 1} + 1\) is prime. - M. F. Hasler, Oct 04 2009

The conclusion \((p(n)).\text{Prime}\) asserts that such a prime \(p\) exists: if no prime satisfies the search conditions then p n is sInf ∅ = 0, which is not prime.

theorem conjecture (n : ℕ) (hn : 1 ≤ n) (h_not_prime : ¬ isFactorialPrime n) :
    (p n).Prime ∧ a n = p n * q n

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

Sources
LeanOeisA55487.conjecture

TheoremDivisibility of \(2^n + 1\) by \(n\)#

A56777 lists composite numbers \(n\) satisfying both \(\varphi(n+12) = \varphi(n) + 12\) and \(\sigma(n+12) = \sigma(n) + 12\).

The conjectures state identities connecting A56777 and prime quadruples (A7530), as well as congruences satisfied by the members of A56777.

References: - A56777

Quoted from FormalConjectures/OEIS/56777.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: 1 open and 3 textbook results. It also has 3 test statements, counted here but not shown.

OeisA56777.a_of_comesFromPrimeQuadruple

Textbook result, proved here.

Numbers coming from prime quadruples are in the sequence A56777.

theorem a_of_comesFromPrimeQuadruple {n : ℕ} (h : ComesFromPrimeQuadruple n) : A n

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

OeisA56777.comesFromPrimeQuadruple_of_a

Open: stated without proof.

All members of the sequence A56777 come from prime quadruples.

theorem comesFromPrimeQuadruple_of_a {n : ℕ} (h : A n) : ComesFromPrimeQuadruple n

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

OeisA56777.mod_72_of_comesFromPrimeQuadruple

Textbook result, proved here.

Numbers coming from prime quadruples satisfy \(n \equiv 65 \pmod{72}\).

theorem mod_72_of_comesFromPrimeQuadruple {n : ℕ} (h : ComesFromPrimeQuadruple n) :
    n % 72 = 65

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

OeisA56777.mod_100_of_comesFromPrimeQuadruple

Textbook result, proved here.

Numbers coming from prime quadruples satisfy \(n \equiv 9 \pmod{100}\), except the first value "65".

theorem mod_100_of_comesFromPrimeQuadruple {n : ℕ} (h65 : 65 < n) (h : ComesFromPrimeQuadruple n) :
    n % 100 = 9

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

Sources
LeanOeisA56777.a_of_comesFromPrimeQuadruple · OeisA56777.comesFromPrimeQuadruple_of_a · OeisA56777.mod_72_of_comesFromPrimeQuadruple · OeisA56777.mod_100_of_comesFromPrimeQuadruple

TheoremNumerator of \(1/\det(M)\) for \(M[i,j] = 1/\operatorname{lcm}(i,j)\)#

Numerator of \(1/\det(M)\) where \(M\) is the \(n \times n\) matrix with \(M[i,j] = 1/\operatorname{lcm}(i,j)\).

References: - A060841 - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.

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

OeisA60841.conjecture1

Open: stated without proof.

"Conjecture: \(1/\det(M)\) is an integer only for n: 1 to 34, 36 and 38." - Robert G. Wilson v, Aug 02 2015

theorem conjecture1 :
    ∀ n : ℕ, 1 ≤ n → (((lcmMatrix n).det)⁻¹.den = 1 ↔ n ∈ integerDetN)

Category research open; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/60841.lean, line 76.

OeisA60841.conjecture2

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA60841_conjecture2.lean#L377.

"All denominators are powers of two (A000079)." - Robert G. Wilson v, Aug 02 2015

This is false: for \(n = 1807\) the denominator of \(1/\det(M)\) is divisible by \(3\). See T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941. The Lean disproof there uses the closed form \(1/\det(M) = \prod_{k=1}^n k^2/\varphi(k)\) from the OEIS entry: https://github.com/epoch-research/LeanOpenProblems-results/blob/fd09021e79869476ef83cda231312f1a2a89c8d7/runs/oeis-full-50usd-ant-j0j0g4uzligm1k41/oeis_60841_conjecture_0/Submission/Spec.lean#L272

theorem conjecture2 :
    ¬ ∀ n : ℕ, 1 ≤ n → ∃ k : ℕ, ((lcmMatrix n).det)⁻¹.den = 2 ^ k

Category research solved; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/60841.lean, line 91.

Sources
LeanOeisA60841.conjecture1 · OeisA60841.conjecture2

TheoremNumber of different products of subsets of \(\{1, 2, \dots, n\}\)#

The number of distinct products (including the empty product 1) of any subset of \(\{1, 2, \dots, n\}\).

References: - A060957 - [Li26] Wentao Li, A counterexample to the A060957 interpolation conjecture, 2026.

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

OeisA60957.counterexample

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/3be119e75ba5b31f034dc0c0b249975d17def711/LeanOeisProofs/NewProofs/A060957.lean#L1479.

An explicit counterexample from [Li26]: both endpoint products occur, but the intermediate product with exponent \(5\) does not. The definitions above specify every parameter, including Counterexample.circuitM as a finite product.

theorem counterexample :
    Counterexample.circuitPrime.Prime ∧ Counterexample.circuitPrime ≤ Counterexample.circuitN ∧
    Counterexample.circuitM ∈ productsOfSubsets Counterexample.circuitN ∧
    Counterexample.circuitPrime ^ 6 * Counterexample.circuitM ∈
      productsOfSubsets Counterexample.circuitN ∧
    0 < (5 : ℕ) ∧ 5 < (6 : ℕ) ∧
    Counterexample.circuitPrime ^ 5 * Counterexample.circuitM ∉
      productsOfSubsets Counterexample.circuitN

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

OeisA60957.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/3be119e75ba5b31f034dc0c0b249975d17def711/LeanOeisProofs/NewProofs/A060957.lean#L1499.

Conjecture: let \(p \le n\) be prime. If \(m\) and \(p^a m\) are two such products, then so is \(p^k m\) for all \(0 < k < a\). - Yan Sheng Ang, Feb 13 2020

This interpolation conjecture is false. Disproved by Wentao Li (2026), with AI assistance; see [Li26]. The counterexample has \(p = 7 \cdot 2^{120} + 1\), \(n = p \cdot 2^{189}\), \(a = 6\), and \(k = 5\).

theorem conjecture :
    ¬ ∀ (n p : ℕ), p.Prime → p ≤ n →
      ∀ (m a_exp : ℕ), m ∈ productsOfSubsets n → p ^ a_exp * m ∈ productsOfSubsets n →
        ∀ k : ℕ, 0 < k → k < a_exp → p ^ k * m ∈ productsOfSubsets n

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

Sources
LeanOeisA60957.counterexample · OeisA60957.conjecture

TheoremReversible multiples \(a(3^n) = 10^{3^{n-2}} - 1\) for powers of \(3\)#

First multiple of \(n\) whose reverse is also divisible by \(n\), or 0 if no such multiple exists.

References: - A062567 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

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

OeisA62567.a_three_pow_eq

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/62567.wip.lean#L324.

The conjecture that \(a(3^n) = 10^{3^{n-2}} - 1\) for \(n > 1\) was shown to be false for \(4 < n < 21\) by Farideh Firoozbakht, who conjectured that for all \(n > 4\), \(a(3^n) \neq 10^{3^{n-2}} - 1\). This latter conjecture is proved here.

A formal proof has been found with the methods described in arxiv/2605.22763.

theorem a_three_pow_eq (n : ℕ) :
    2 ≤ n → (a (3 ^ n) = 10 ^ (3 ^ (n - 2)) - 1 ↔ n = 2 ∨ n = 3 ∨ n = 4)

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

Sources
LeanOeisA62567.a_three_pow_eq

TheoremConjectures associated with A063880#

A063880 lists numbers \(n\) such that \(\sigma(n) = 2 \cdot \text{usigma}(n)\), where \(\sigma(n)\) is the sum of all divisors and \(\text{usigma}(n)\) is the sum of unitary divisors.

Equivalently, these are numbers whose unitary and non-unitary divisors have equal sum.

The conjectures state that all members satisfy \(n \equiv 108 \pmod{216}\), and that all primitive terms (those whose proper divisors aren't in the sequence) are powerful numbers, with \(108\) being the only primitive term.

References: - A063880

Quoted from FormalConjectures/OEIS/63880.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: 2 open, 1 solved and 2 textbook results. It also has 4 test statements and 6 API statements, counted here but not shown.

OeisA63880.mod_216_of_a

Open: stated without proof.

All members of the sequence satisfy \(n \equiv 108 \pmod{216}\).

theorem mod_216_of_a {n : ℕ} (h : A n) : n % 216 = 108

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

OeisA63880.powerful_of_isPrimitiveTerm

Textbook result, proved here.

All primitive terms are powerful numbers: if p divided n exactly once, then n / p would also be in the sequence.

theorem powerful_of_isPrimitiveTerm {n : ℕ} (h : IsPrimitiveTerm n) : n.Powerful

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

OeisA63880.unique_primitive_108

Open: stated without proof.

\(108\) is the only primitive term.

theorem unique_primitive_108 {n : ℕ} (h : IsPrimitiveTerm n) : n = 108

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

OeisA63880.a_of_primitive_mul_squarefree

Textbook result, proved here.

If \(m\) is a primitive term and \(s\) is squarefree with \(\gcd(m, s) = 1\), then \(m \cdot s\) is in the sequence.

theorem a_of_primitive_mul_squarefree (m s : ℕ) (hm : IsPrimitiveTerm m)
    (hs : Squarefree s) (hcoprime : m.Coprime s) : A (m * s)

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

OeisA63880.exists_primitive_of_a

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA63880_exists_primitive_of_a.lean#L491.

Non-primitive terms have the form \(m \cdot s\) where \(m\) is primitive and \(s\) is squarefree with \(\gcd(m, s) = 1\).

theorem exists_primitive_of_a {n : ℕ} (h : A n) :
    ∃ m s, IsPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s

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

Sources
LeanOeisA63880.mod_216_of_a · OeisA63880.powerful_of_isPrimitiveTerm · OeisA63880.unique_primitive_108 · OeisA63880.a_of_primitive_mul_squarefree · OeisA63880.exists_primitive_of_a

TheoremNumerator - denominator in \(n\)-th harmonic number#

\(a(n) = \text{numerator}(H_n) - \text{denominator}(H_n)\), where \(H_n = 1 + 1/2 + \dots + 1/n\).

References: - A064169

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

OeisA64169.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_64169_conjecture_0/Submission/Spec.lean#L514.

"Conjecture: for \(n > 2\), \(n\) divides \(a(n-2)\) if and only if \(n\) is a prime. Checked up to 20000. - Amiram Eldar and Thomas Ordowski, Jul 27 2019

This is false for the composite number \(16843^2\).

theorem conjecture : ¬ ∀ (n : ℕ), 2 < n → ((n : ℤ) ∣ a (n - 2) ↔ n.Prime)

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

Sources
LeanOeisA64169.conjecture

TheoremInteger part of area of a regular polygon with \(n\) sides each of length 1#

The area of a regular \(n\)-gon with side length 1 is given by \(\frac{n}{4} \cot(\pi / n) = \frac{n}{4 \tan(\pi / n)}\).

References: - A064313

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

OeisA64313.conjecture

Open: stated without proof.

"Usually (perhaps always?) \(\lfloor n^2 / (4\pi) - \pi / 12 \rfloor\) for a polygon of circumference \(n\). Note that the area of a circle with circumference \(C\) is \(C^2 / (4\pi)\)."

theorem conjecture (n : ℕ) (hn : 3 ≤ n) :
    a n = (Int.floor ((n : ℝ) ^ 2 / (4 * Real.pi) - Real.pi / 12)).toNat

Category research open; AMS 51 Geometry. Declared in FormalConjectures/OEIS/64313.lean, line 110.

Sources
LeanOeisA64313.conjecture

TheoremDecimal encoding of the prime factorization of \(n\)#

If \(n\) has prime factorization \(p_1^{e_1} \dots p_r^{e_r}\) with \(p_1 < \dots < p_r\), then its decimal encoding is \(p_1 e_1 \dots p_r e_r\).

References: - A067599

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

OeisA67599.conjecture

Open: stated without proof.

"\(a(31) = a(177147) = 311\). Is there any solution to \(a(n) = n\)? - Franklin T. Adams-Watters, Dec 18 2006"

theorem conjecture :
    ∃ n : ℕ, 2 ≤ n ∧ a n = n

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

Sources
LeanOeisA67599.conjecture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.