A logarithmic derivative with… to Decimal concatenation of a…
TheoremA logarithmic derivative with prime-divisible coefficients#
Let \(F(x)\) be the generating function of A381353, with \(F(0)=1\), \([x]F(x)=1\), and \([x^n]F(x)^{p_n}=0\) for \(n>1\), where \(p_n\) is the \(n\)-th prime. The sequence is defined by \(\sum_{n\ge1}a(n)x^n=xF'(x)/F(x)\).
References: - A381355 - A381353 - [Li26] Wentao Li, Prime divisibility of logarithmic-derivative coefficients, 2026.
Quoted from FormalConjectures/OEIS/381355.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.
OeisA381355.conjecture
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewProofs/A381355.lean#L380.
"Conjecture: \(a(n)\) is divisible by \(\operatorname{prime}(n)\) for \(n > 1\)." - Paul D. Hanna, Mar 11 2025.
Proved and formalized in Lean by Wentao Li, with AI assistance; see [Li26].
theorem conjecture (n : ℕ) (hn : 1 < n) : (primeN n : ℤ) ∣ a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/381355.lean, line 235.
Sources
TheoremPeriodicity of \(k\)-th prime factors in coupled nonlinear recurrence \(a(n)\)#
The sequence \(a(n)\) is defined by \(a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)\) where \(b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)\), with \(a(0) = b(0) = b(1) = 1\) and \(a(1) = 2\).
References: - A382590 - mathoverflow/490330: B. Morga, "Peculiar family of recurrence formula where for \(n>1\) if you take the \(n\)-th prime factor of each term, you get an eventually periodic sequence", Mar. 31, 2025.
Quoted from FormalConjectures/OEIS/382590.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, counted here but not shown.
OeisA382590.kthPrimeFactor_periodic
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewFormalization/A382590.lean#L201.
Conjecture: For any \(k > 1\), if you take the \(k\)-th prime factor of each term, you get an eventually periodic sequence. - Bryle Morga, Mar 31 2025
Here the \(k\)-th prime factor of \(a(n)\) is the \(k\)-th smallest distinct prime divisor of \(|a(n)|\); for example the second prime factors of \(a(5) = 18\), \(a(6) = 20\) and \(a(7) = 896\) are \(3\), \(5\) and \(7\).
This was proved by Terence Tao in a MathOverflow answer, using that \(a(n)\) divides \(a(n+3)\) for all \(n\). Lean formalization by Wentao Li, with AI assistance.
theorem kthPrimeFactor_periodic : ∀ k : ℕ, k ≥ 2 → ∃ N₀ p : ℕ, p > 0 ∧
∀ n : ℕ, n ≥ N₀ → kthPrimeFactor k (a (n + p)) = kthPrimeFactor k (a n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/382590.lean, line 114.
Sources
TheoremLengths of the 2-dense sublists of divisors of \(n\)#
Write the divisors of \(n\) in increasing order and split this list between consecutive divisors \(d < d'\) with \(d' > 2d\). The pieces are the 2-dense sublists of divisors of \(n\). Row \(n\) of the triangle lists their lengths. Row \(n\) of A384225 lists the numbers of odd terms in them.
Quoted from FormalConjectures/OEIS/384222.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 7 test statements, counted here but not shown.
OeisA384222.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/otoi-lab/oeis-lean-proofs/blob/14f275b8b370bcf76213de10bb3f8fda84a6461e/OeisProofs/FC/A384222.lean#L26-L31.
"Conjecture 1: row n is a palindromic composition of A000005(n)."
A composition of \(A000005(n)\) is a list of positive integers with sum \(A000005(n)\), the number of divisors of \(n\).
Solved by Claude (Anthropic) prompted by otoinobuo. The map \(d \mapsto n/d\) reverses the list of divisors and preserves the ratio of consecutive divisors.
theorem conjecture_1 (n : ℕ) (hn : 0 < n) :
(∀ k ∈ row n, 0 < k) ∧ (row n).sum = n.divisors.card ∧ (row n).reverse = row n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/384222.lean, line 82.
OeisA384222.conjecture_formula
Solved: stated here; a Lean proof is at https://github.com/otoi-lab/oeis-lean-proofs/blob/14f275b8b370bcf76213de10bb3f8fda84a6461e/OeisProofs/FC/A384222.lean#L33-L36.
"T(n,k) = A384225(n,k) * A001511(n) = A384225(n,k) * A000005(n) / A001227(n). (conjectured)." - Omar E. Pol, Apr 13 2026
This formalizes the first equality. The ruler function is \(A001511(n) = \nu_2(n) + 1\).
Solved by Claude (Anthropic) prompted by otoinobuo. If \(d\) and \(2d\) divide \(n\), then they lie in the same 2-dense sublist. So each sublist is a union of sets \(\{o, 2o, \dots, 2^{\nu_2(n)} o\}\) with \(o\) odd.
theorem conjecture_formula (n : ℕ) (hn : 0 < n) :
row n = (oddRow n).map ((padicValNat 2 n + 1) * ·)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/384222.lean, line 99.
Sources
TheoremA differential generating function#
The generating function satisfies \(A(x)=x+(xA(x)^2)'\). Its constant term is zero. Seiichi Manyama's recurrence is \(a(1)=1\) and \(a(n)=(n+1)\sum_{k=1}^{n-1}a(k)a(n-k)\) for \(n>1\).
References: - A397588 - [Li26] Wentao Li, Parity and divisibility for A397588, 2026.
Quoted from FormalConjectures/OEIS/397588.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 and 2 API statements, counted here but not shown.
OeisA397588.conjecture_parity
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewFormalization/A397588.lean#L211.
"Conjecture: \(a(n)\) is odd iff \(n\) is a power of \(2\) for \(n \ge 1\)." - Paul D. Hanna, Jul 03 2026.
Lean formalization by Wentao Li, with AI assistance; see [Li26].
theorem conjecture_parity (n : ℕ) (hn : 1 ≤ n) :
Odd (a n) ↔ ∃ k : ℕ, n = 2 ^ k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/397588.lean, line 107.
OeisA397588.three_dvd_a
Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/0a23974e54b90afd1453ef02c27cf8f617bad940/LeanOeisProofs/NewFormalization/A397588.lean#L325.
"\(a(n)\) divisible by \(3\) for \(n > 1\)." - Paul D. Hanna, Jul 03 2026.
Lean formalization by Wentao Li, with AI assistance; see [Li26].
theorem three_dvd_a (n : ℕ) (hn : 1 < n) : 3 ∣ a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/397588.lean, line 120.
Sources
TheoremMaximum number of terms in a 2-dense sublist of divisors of \(n\)#
Write the divisors of \(n\) in increasing order and split this list between consecutive divisors \(d < d'\) with \(d' > 2d\). The pieces are the 2-dense sublists of divisors of \(n\). The sequence gives the maximum number of terms in such a sublist.
Quoted from FormalConjectures/OEIS/400194.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, counted here but not shown.
OeisA400194.conjecture
Solved: stated here; a Lean proof is at https://github.com/otoi-lab/oeis-lean-proofs/blob/14f275b8b370bcf76213de10bb3f8fda84a6461e/OeisProofs/FC/A400194.lean#L26-L27.
"Conjecture: a(n) is the product of the ruler function of n and the maximum number of odd terms in a 2-dense sublist of divisors of n."
"Conjecture: a(n) = A001511(n) * A400195(n)."
The ruler function is \(A001511(n) = \nu_2(n) + 1\).
Solved by Claude (Anthropic) prompted by otoinobuo. If \(d\) and \(2d\) divide \(n\), then they lie in the same 2-dense sublist. So each sublist is a union of sets \(\{o, 2o, \dots, 2^{\nu_2(n)} o\}\) with \(o\) odd.
theorem conjecture (n : ℕ) (hn : 0 < n) : a n = (padicValNat 2 n + 1) * b n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/400194.lean, line 86.
Sources
TheoremDecimal concatenation of a cofactor and the largest prime factor#
For a composite positive integer \(n\), let \(p\) be its largest prime factor. The sequence value \(a(n)\) concatenates the decimal representations of \(n/p\) and \(p\), in that order. It fixes primes and one, and is extended here by \(a(0)=0\). OEIS A397122 records the prime reached by iterating this map from each starting value, or \(-1\) if no prime is reached.
References: - OEIS A401006 - OEIS A397122
Quoted from FormalConjectures/OEIS/401006.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 5 API statements, counted here but not shown.
OeisA401006.eventually_prime
Open: stated without proof.
If we start at \(n \ge 2\), and repeatedly apply the map \(k \mapsto a(k)\), we will eventually reach a prime, which is then a fixed point.
theorem eventually_prime : ∀ n : ℕ, 2 ≤ n → ReachesPrime n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/401006.lean, line 214.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.