Nonnegativity of the Dirichlet… to A cubic generating function…

TheoremNonnegativity of the Dirichlet square root of A046644#

A317940 is the integer sequence whose value a n is the numerator of the rational sequence f n, where the Dirichlet convolution square of f is A046644. The auxiliary sequence A046644 is multiplicative and takes the value \(2^{\operatorname{A005187}(e)}\) on a prime power \(p^e\).

The conjecture asks whether f n is nonnegative for every positive n. The proof reduces the problem to prime powers and constructs positive rational coefficients \(c(e)\) satisfying

\[\sum_{i=0}^e c(i)c(e-i)=2^{\operatorname{A005187}(e)}.\]

The coefficients are obtained from formal power series. A positive series \(A\) is defined by the first-order differential equation \(A' = \frac12 D A\). A second explicitly defined series \(B\) satisfies \(B' = D B\) and has the same constant term as \(A^2\); uniqueness of the coefficient recurrence therefore gives \(A^2=B\). After rescaling the coefficients by \(4^e\), this becomes the displayed prime-power convolution identity.

Extending \(c(e)\) multiplicatively over prime factorizations gives a positive arithmetic function root with root * root = a046644. Finally, the recursive definition of f is shown to be the unique Dirichlet square root with value one at \(1\), so f = root and every positive-index value of f is positive.

This route was found by first exploiting the multiplicativity recorded in the OEIS entry, reducing the recurrence to the exponent of a single prime, and then recognizing the resulting coefficient identities as a formal-power-series differential equation.

References: - A317940 - A046644 - A005187

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

OeisA317940.f_nonnegative

Solved: stated here; a Lean proof is at https://domthedeveloper.github.io/crl/math/a317940/proof/A317940_verified.lean.

"No negative terms among the first 2^20 terms. Is the sequence nonnegative?"

Equivalently, the rational Dirichlet square root f is nonnegative at every positive index. Informally, the proof constructs a strictly positive multiplicative square root prime-power by prime-power using formal power series, and then identifies it with the recursively defined sequence f.

The proof was obtained by exploiting the multiplicativity of A046644 and reducing the problem to its values on prime powers. The resulting convolution recurrence for the prime-power coefficients was recognized as a formal-power-series identity. A positive coefficient sequence was constructed through a differential equation for the generating series, extended multiplicatively to all positive integers, and finally identified with the recursively defined Dirichlet square root by uniqueness.

theorem f_nonnegative (n : ℕ) (h : n > 0) : f n ≥ 0

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

Sources
LeanOeisA317940.f_nonnegative

TheoremPronic indices for odd coefficients of \(\sum_{n \ge 0} x^n \frac{(1+x^n)^n}{(1+x^{n+1})^{n+1}}\)#

Coefficients of G.f. \(\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}\). The \(m\)-th term \(a(m)\) is the coefficient of \(x^m\), which is explicitly given by the sum:

\[ a(m) = \sum_{n=0}^m \sum_{k=0}^n \binom{n}{k} (-1)^j \binom{n+j}{j},\]

where \(j = \frac{m - n(k+1)}{n+1}\), and the term is zero unless \(j\) is a natural number.

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

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

OeisA323557.odd_a_implies_pronic

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

Conjecture: Odd terms occur only at positions \(n(n+1)\) for \(n \ge 0\) (verified for initial 32600 terms).

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

This statement is equivalent to OeisA325046.odd_a_implies_pronic. The two sequences differ only by the sign \((-1)^j\) on each summand, so they agree modulo \(2\) and have the same odd indices.

theorem odd_a_implies_pronic (m : ℕ) : Odd (a m) → ∃ n : ℕ, m = n * (n + 1)

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

Sources
LeanOeisA323557.odd_a_implies_pronic

TheoremPronic indices for odd coefficients of \(\sum_{n \ge 0} x^n \frac{(1+x^n)^n}{(1-x^{n+1})^{n+1}}\)#

Coefficients of G.f. \(\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}\).

The term \(a(N)\) is the coefficient of \(x^N\) in the generating function. Expanding the terms, we get a formula for \(a(N)\):

\[a(N) = \sum_{n=0}^N \sum_{k=0}^n \mathbf{1}_{n + nk + (n+1)j = N} \binom{n}{k} \binom{n+j}{j}\]

where \(j = \frac{N - n(k+1)}{n+1}\).

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

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

OeisA325046.odd_a_implies_pronic

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

Conjecture: Odd terms occur only at positions \(n(n+1)\) for \(n \ge 0\).

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

This statement is equivalent to OeisA323557.odd_a_implies_pronic. The two sequences differ only by the sign \((-1)^j\) on each summand, so they agree modulo \(2\) and have the same odd indices.

theorem odd_a_implies_pronic (N : ℕ) : a N % 2 = 1 → ∃ k : ℕ, N = k * (k + 1)

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

Sources
LeanOeisA325046.odd_a_implies_pronic

TheoremTripling until the seed's digits reappear#

Starting with the least positive integer not used previously, repeatedly triple it and stop the block at the first positive power whose decimal expansion contains the seed's digits. Then repeat from the new least missing positive integer.

References: - A331631

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

OeisA331631.conjecture

Open: stated without proof.

OEIS A331631 states: The sequence is conjectured to be a permutation of the positive integers (see the Crossrefs section).

theorem conjecture :
    ∃ a : ℕ → ℕ, FollowsRule a ∧ Function.Injective a ∧
      ∀ k > 0, ∃ n, a n = k

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

Sources
LeanOeisA331631.conjecture

TheoremConvergence of fraction numerators \(a(n)/b(n)\) to \(e\)#

a: Numerators of a sequence of fractions converging to \(e\).

\[a(1) = 3, a(2) = 5\]

For \(n > 2\):

\[a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - \left(\frac{n-2}{2}\right) a(n-3) & \text{if } n \text{ is even} \cr 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}\]

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

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

OeisA340737.tendsto_exp_one

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

Conjecture: \(\lim_{n \to \infty} a(n) / b(n) = e\), where \(b(n)\) is the companion denominator sequence.

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

theorem tendsto_exp_one :
    Filter.Tendsto (fun n : ℕ => (a n : ℝ) / (b n : ℝ)) Filter.atTop (nhds (Real.exp 1))

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

Sources
LeanOeisA340737.tendsto_exp_one

TheoremBounds on fractional parts \(n r^2 - a(n)\) for \(r = (2+\sqrt{5})/2\)#

\(a(n) = \lfloor r \cdot \lfloor r \cdot n \rfloor \rfloor\), where \(r = (2 + \sqrt{5})/2\).

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

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

OeisA341254.a_bounds

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

Conjecture: \(1/4 < n r^2 - a(n) < 3\) for \(n \ge 1\), where \(r = (2 + \sqrt{5})/2\).

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

theorem a_bounds (n : ℕ) (hn : 1 ≤ n) : (1 / 4 : ℝ) < (n : ℝ) * rSq - (a n : ℝ) ∧
    (n : ℝ) * rSq - (a n : ℝ) < 3

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

Sources
LeanOeisA341254.a_bounds

TheoremNumerator of a sum involving binomial coefficients#

\(a(n)\) is the numerator of \(\sum_{k = 1}^n \frac{1}{k^3} \binom{n}{k}^2 \binom{n+k}{k}^2\) for \(n \ge 1\) with \(a(0) = 0\).

References: - A357513

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

OeisA357513.a357513_supercongruence

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/9c7f21e7d4445637538bc1817b058b9b3f31bd2b/FormalConjectures/OEIS/357513.lean#L232.

We have \(a(p-1) \equiv 0 \pmod{p^4}\) for all primes \(p \ge 3\) except \(p=7\).

proved by AlphaProof

theorem a357513_supercongruence (p : ℕ) (hp : p.Prime) (h_ge3 : p ≥ 3) (h_neq7 : p ≠ 7) :
    (a (p - 1) : ℤ) ≡ 0 [ZMOD (p : ℤ) ^ 4]

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

OeisA357513.general_supercongruence

Open: stated without proof.

We conjecture that \(u(p-1) == 0 (mod p^4)\) for all primes \(p\), with a finite number of exceptions that depend on \(m\).

theorem general_supercongruence (m : ℕ) : ∃ (exceptions : Finset ℕ), ∀ p, p.Prime →
    p ∉ exceptions → u m (p - 1) = (0 : ZMod (p ^ 4))

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

Sources
LeanOeisA357513.a357513_supercongruence · OeisA357513.general_supercongruence

TheoremFactor bounds for Fermat numbers#

\(a(n)\) is the minimum integer \(k\) such that the smallest prime factor of the \(n\)-th Fermat number exceeds \(2^{2^n - k}\).

References: - A358684 - SA22 Lorenzo Sauras-Altuzarra, Some properties of the factors of Fermat numbers, Art Discrete Appl. Math. (2022).

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

OeisA358684.oeis_358684_conjecture_0

Proved here.

Conjecture: the dyadic valuation of A93179(n) - 1 does not exceed 2^n - a(n).

A93179(n) is minFac(fermatNumber n), the smallest prime factor of the n-th Fermat number. The conjecture states that if \(P_n\) is the smallest prime factor of the \(n\)-th Fermat number, then \(\nu_2(P_n - 1) \le 2^n - a(n)\). Substituting the definition of \(a(n)\), this is equivalent to \(\nu_2(P_n - 1) \le \lfloor \log_2(P_n) \rfloor\).

This is Conjecture 3.4 in [SA22].

theorem oeis_358684_conjecture_0 (n : ℕ) :
    padicValNat 2 (minFac (fermatNumber n) - 1) ≤ 2 ^ n - a n

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

Sources
LeanOeisA358684.oeis_358684_conjecture_0

TheoremA factorial ratio analogous to the Catalan numbers#

The sequence is defined by \(a(n)=3(4n)!/(n!((n+1)!)^3)\) for \(n \ge 0\).

References: - A361033 - [Li26] Wentao Li, Integrality and parity of a factorial ratio, 2026.

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

OeisA361033.conjecture_1

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewFormalization/A361033.lean#L380.

The parity conjecture: "Conjecture: \(a(n)\) is odd iff \(n = 2^k - 1\) for some \(k \ge 0\)." - Peter Bala, Mar 01 2023.

Proved and formalized in Lean by Wentao Li, with AI assistance; see [Li26].

theorem conjecture_1 (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k - 1

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

Sources
LeanOeisA361033.conjecture_1

TheoremPrimality of continued fraction denominators \(a(n)\) for \(n \ge 3\)#

Auxiliary sequence A051403, defined as

\[\frac{(n+2) \sum_{k=0}^n k!}{2}\]

Denominator of the continued fraction \(1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))\). The sequence is defined by the formula:

\[a(n) = \frac{n^2 - 2}{\gcd(n^2 - 2, 2 \cdot A051403(n-3) + n \cdot A051403(n-4))}\]

The formula is valid for \(n \ge 3\).

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

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

OeisA363102.a_eq_one_or_prime

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

Conjecture: The sequence contains only 1's and primes.

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

theorem a_eq_one_or_prime : ∀ n : ℕ, 3 ≤ n → a n = 1 ∨ Nat.Prime (a n)

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

Sources
LeanOeisA363102.a_eq_one_or_prime

TheoremRealization of primes \(p \equiv \pm 1 \pmod{10}\) by continued fraction denominators#

\(a(n)\) is the denominator of the finite continued fraction

\[\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{-4}}}}}}\]

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

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

OeisA363347.exists_a_eq_prime

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

Conjecture: The sequence contains all prime numbers which end with a 1 or 9 (i.e., primes \(p \equiv 1\) or \(9 \pmod{10}\)).

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

theorem exists_a_eq_prime :
    ∀ p : ℕ, (p.Prime ∧ (p ≡ 1 [MOD 10] ∨ p ≡ 9 [MOD 10])) → ∃ n : ℕ, a n = p

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

Sources
LeanOeisA363347.exists_a_eq_prime

TheoremA generating function with powers two and three#

The sequence consists of the coefficients of \(A(x)=1+x(A(x)^2-A(-x)^2)/2+x(A(x)^3+A(-x)^3)/2\).

References: - A368626 - [Li26] Wentao Li, Generating-function bridge and parity for A368626, 2026.

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

OeisA368626.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/9d4a205da2a4094800f9c600a7b0b5223eda51ce/LeanOeisProofs/NewProofs/A368626.lean#L529.

"Conjecture: \(a(n)\) is odd when \(n = 2^k - 1\) for \(k \ge 0\) and even elsewhere." - Paul D. Hanna, Jan 09 2024.

Lean proof by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k - 1

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

Sources
LeanOeisA368626.conjecture

TheoremA generating function with powers two and four#

The sequence consists of the coefficients of \(A(x)=1+x(A(x)^2-A(-x)^2)/2+x(A(x)^4+A(-x)^4)/2\).

References: - A368628 - [Li26] Wentao Li, Generating-function bridge and parity for A368628, 2026.

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

OeisA368628.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/b5eabe63ce276d12170d18f91b5b7327130c4cbe/LeanOeisProofs/NewFormalization/A368628.lean#L523.

"Conjecture: \(a(n)\) is odd when \(n = (4^k - 1)/3\) for \(k \ge 0\), and even elsewhere." - Paul D. Hanna, Jan 10 2024.

Lean formalization by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = (4 ^ k - 1) / 3

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

Sources
LeanOeisA368628.conjecture

TheoremA generating function with powers two and four#

The sequence consists of the coefficients of \(A(x)=1+x(A(x)^2+A(-x)^2)/2+x(A(x)^4-A(-x)^4)/2\).

References: - A368629 - [Li26] Wentao Li, Generating-function bridge and parity for A368629, 2026.

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

OeisA368629.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/9d4a205da2a4094800f9c600a7b0b5223eda51ce/LeanOeisProofs/NewProofs/A368629.lean#L463.

"Conjecture: \(a(n)\) is odd when \(n = 2^k - 1\) for \(k \ge 0\), and even elsewhere." - Paul D. Hanna, Jan 10 2024.

Lean proof by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k - 1

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

Sources
LeanOeisA368629.conjecture

TheoremA quadratic generating function with sign substitution#

The sequence consists of the coefficients of \(A(x)=1+2xA(x)^2-xA(-x)^2\).

References: - A368633 - [Li26] Wentao Li, Catalan parity for A368633, 2026.

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

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

OeisA368633.conjecture_1

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewFormalization/A368633.lean#L166.

The parity conjecture (Conjecture 1): "Conjecture: \(a(n)\) is odd when \(n = 2^k - 1\) for \(k \ge 0\) and even elsewhere." - Paul D. Hanna, Jan 11 2024.

Lean formalization by Wentao Li, with AI assistance; see [Li26].

theorem conjecture_1 (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n + 1 = 2 ^ k

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

Sources
LeanOeisA368633.conjecture_1

TheoremA generating function with signed square terms#

The sequence consists of the coefficients of \(A(x)=1+x(3A(x)^2-A(-x)^2)/2\).

References: - A368634 - [Li26] Wentao Li, Generating-function bridge and parity for A368634, 2026.

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

OeisA368634.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/9d4a205da2a4094800f9c600a7b0b5223eda51ce/LeanOeisProofs/NewProofs/A368634.lean#L407.

"Conjecture: \(a(n)\) is odd when \(n = 2^k - 1\) for \(k \ge 0\) and even elsewhere." - Paul D. Hanna, Jan 12 2024.

Lean proof by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k - 1

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

Sources
LeanOeisA368634.conjecture

TheoremThe generating function \(A(x)=1+3xA(x)^2-2xA(-x)^2\)#

The sequence consists of the coefficients of \(A(x)=1+3xA(x)^2-2xA(-x)^2\).

References: - A368635 - [Li26] Wentao Li, Generating-function bridge and parity for A368635, 2026.

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

OeisA368635.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/9d4a205da2a4094800f9c600a7b0b5223eda51ce/LeanOeisProofs/NewFormalization/A368635.lean#L433.

"Conjecture: \(a(n)\) is odd when \(n = 2^k - 1\) for \(k \ge 0\), and even elsewhere." - Paul D. Hanna, Jan 12 2024.

Lean proof by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) : Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k - 1

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

Sources
LeanOeisA368635.conjecture

TheoremIntegrality of the factorial ratio \(\frac{(12n+6)! (6n+9)!}{108 (4n+2)! (2n+3)! ((6n+5)!)^2}\)#

The factorial ratio

\[a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot (2n + 3)! \cdot ((6n + 5)!)^2}\]

It is conjectured that \(a(n)\) are integers.

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

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

OeisA368692.a_is_int

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

It is conjectured here that \(a(n)\) are integers.

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

theorem a_is_int (n : ℕ) : 108 * ((4 * n + 2)! * (2 * n + 3)! * ((6 * n + 5)!) ^ 2) ∣
    (12 * n + 6)! * (6 * n + 9)!

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

Sources
LeanOeisA368692.a_is_int

TheoremUnique realization of odd primes \(p \notin \{3, 5\}\) by continued fraction values#

\(a(n)\) is the denominator of the finite continued fraction

\[\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}}\]

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

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

OeisA372761.exists_unique_a_eq_prime

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

Conjecture: Except for 3 and 5, all odd primes appear in the sequence once. - Thomas Scheuerle, May 11 2024

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

theorem exists_unique_a_eq_prime :
    ∀ p : ℕ, Nat.Prime p ∧ p % 2 = 1 ∧ p ≠ 3 ∧ p ≠ 5 → ∃! n, n ≥ 3 ∧ a n = p

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

Sources
LeanOeisA372761.exists_unique_a_eq_prime

TheoremA cubic generating function with ternary substitution#

The coefficients of the generating function \(A(x)=x+x^2+(2A(x)^3+A(x^3))/3\), with constant term \(a(0)=0\).

References: - A375439 - A038754 - [Li26] Wentao Li, Parity of A375439, 2026.

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

OeisA375439.conjecture

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewProofs/A375439.lean#L382.

"Conjecture: \(a(n)\) is odd iff \(n\) is in A038754, which consists of numbers of the form \(3^k\) and \(2*3^k\)." - Paul D. Hanna, Aug 21 2024.

Lean proof by Wentao Li, with AI assistance; see [Li26].

theorem conjecture (n : ℕ) (hn : 1 ≤ n) :
    Odd (a n) ↔ ∃ k : ℕ, n = 3 ^ k ∨ n = 2 * 3 ^ k

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

Sources
LeanOeisA375439.conjecture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.