Density of ones in the… to Primes congruent to ${3, 5…

TheoremDensity of ones in the Kolakoski sequence #

The Kolakoski sequence is the self-describing sequence of ones and twos whose terms are the lengths of its successive runs. Its official indexing begins with $a(1) = 1$; here it is extended by $a(0) = 0$.

References: - A000002 - E. S. Kupin and E. S. Rowland, "Bounds on the frequency of 1 in the Kolakoski word", arXiv:0809.2776 [math.CO] (2008).

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

`OeisA2.density_one`

Open: stated without proof.

"It is an unsolved problem to show that the density of 1's is equal to 1/2." — A000002

theorem density_one : {n : ℕ | a n = 1}.HasDensity (1 / 2 : ℝ)

Category research open; AMS 11 Number theory, 68 Computer science. Declared in FormalConjectures/OEIS/2.lean, line 137.

Sources

LeanOeisA2.density_one

TheoremThe prime numbers #

The $n$-th prime number $p_n$, where $p_1 = 2$.

References: - A000040

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

`OeisA40.conjecture`

Open: stated without proof.

Conjecture from Thomas Ordowski (2023): $\log \log a(n+1) - \log \log a(n) < 1/n$ for $n > 0$.

theorem conjecture (n : ℕ) (hn : 0 < n) :
    Real.log (Real.log (a (n + 1) : ℝ)) - Real.log (Real.log (a n : ℝ)) < 1 / (n : ℝ)

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

Sources

LeanOeisA40.conjecture

TheoremNo powers as partition numbers #

There are no partition numbers $a(k)$ of the form $x^m$, with $x,m$ integers $>1$.

Reference: A41

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

`OeisA41.noPowerPartitionNumber`

Open: stated without proof.

There are no partition numbers $a(k)$ of the form $x^m$, with $x,m$ integers $>1$. See comment by Zhi-Wei Sun (Dec 02 2013).

theorem noPowerPartitionNumber : ∀ k, ¬IsPerfectPower (partitionNumber k)

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

Sources

LeanOeisA41.noPowerPartitionNumber

TheoremFractional parts of sums of reciprocals of Catalan numbers $C(n)$#

Catalan numbers $C(n) = \frac{1}{n+1}\binom{2n}{n}$.

The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers.

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

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

`OeisA108.catalanReciprocalSum_fracPart_inj`

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

Conjecture: All the rational numbers $\sum_{i=j}^k \frac{1}{a(i)}$ with $0 < \min\{2,k\} \le j \le k$ have pairwise distinct fractional parts.

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

theorem catalanReciprocalSum_fracPart_inj : ∀ ⦃j₁ k₁ j₂ k₂ : ℕ⦄,
    IndexCond j₁ k₁ → IndexCond j₂ k₂ →
    (j₁, k₁) ≠ (j₂, k₂) →
    fracPart (catalanReciprocalSum j₁ k₁) ≠ fracPart (catalanReciprocalSum j₂ k₂)

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

Sources

LeanOeisA108.catalanReciprocalSum_fracPart_inj

TheoremNumber of squares $\bmod n$#

The number of squares modulo $n$. This is the cardinality of the set $\{k^2 \bmod n \mid k \in \{0, 1, \dots, n-1\}\}$.

References: - A000224

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

`OeisA224.conjecture`

Open: stated without proof.

$n^2 \equiv 1 \pmod{a(n)(a(n)-1)}$ if and only if $n$ is an odd prime. - Thomas Ordowski, Jun 08 2017

theorem conjecture (n : ℕ) (hn : 1 < n) :
    (n.Prime ∧ n ≠ 2) ↔ n ^ 2 ≡ 1 [MOD a n * (a n - 1)]

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

Sources

LeanOeisA224.conjecture

TheoremEuclid-Mullin sequence #

The Euclid-Mullin sequence starts with $a(1) = 2$. Each subsequent term is the smallest prime factor of one plus the product of all preceding terms. We extend the sequence by $a(0) = 1$ and write $b(n)$ for the product of the first $n$ official terms.

References: - A000945 - [Mullin63] A. A. Mullin, "Research Problem 8 (ii)", Bull. Amer. Math. Soc. 69 (1963), p. 737. - [Wagstaff93] S. S. Wagstaff, Jr., "Computing Euclid's primes", Bull. Institute Combin. Applications 8 (1993), pp. 23-32. - [CrandallPomerance01] R. Crandall and C. Pomerance, Prime Numbers: A Computational Perspective, Springer (2001), p. 6. - A. R. Booker, "A variant of the Euclid-Mullin sequence containing every prime," arXiv:1605.08929, Journal of Integer Sequences 19 (2016), Article 16.6.4.

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

`OeisA945.every_prime_occurs`

Open: stated without proof.

"Does the sequence ... contain every prime? ... [It] was considered by Guy and Nowakowski and later by Shanks, [Wagstaff93] computed the sequence through the 43rd term. The computational problem inherent in continuing the sequence further is the enormous size of the numbers that must be factored. Already the number $a(1) \cdots a(43) + 1$ has 180 digits." - [CrandallPomerance01]

See also [Mullin63].

theorem every_prime_occurs :
    ∀ p, p.Prime → ∃ n ≥ 1, a n = p

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

Sources

LeanOeisA945.every_prime_occurs

Theorem$a(n) = 2^(2^n)$#

References: - A001146

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

`OeisA1146.divisibility_fact`

Proved here.

The forward direction: if $k = a(n)$ for $n \ge 2$, then $k^4 - 1$ divides $2^k - 1$.

theorem divisibility_fact (n : ℕ) (hn : 2 ≤ n) : (((a n)^4 - 1) : ℕ) ∣ (2^(a n) - 1 : ℕ)

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

`OeisA1146.conjecture`

Open: stated without proof.

I conjecture that { $a(n)$ ; $n>1$ } are the numbers such that $n^4-1$ divides $2^n-1$, intersection of A247219 and A247165. - M. F. Hasler, Jul 25 2015 This formalizes the reverse direction.

theorem conjecture :
  ∀ k : ℕ, ((k^4 - 1) : ℕ) ∣ (2^k - 1 : ℕ) → k > 1 → ∃ n : ℕ, 2 ≤ n ∧ k = a n

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

Sources

LeanOeisA1146.divisibility_fact · OeisA1146.conjecture

TheoremSum of squares of divisors of $n$#

References: - A001157

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

`OeisA1157.conjecture`

Open: stated without proof.

Conjecture: For each k = 2,3,..., all the rational numbers $\frac{\sigma_k(n)}{n^k} = \sum_{d|n} \frac{1}{d^k}$ (n = 1,2,3,...) have pairwise distinct fractional parts. - Zhi-Wei Sun, Oct 15 2015

theorem conjecture :
  ∀ k : ℕ, 2 ≤ k →
    ∀ n₁ n₂ : ℕ, 0 < n₁ → 0 < n₂ → n₁ ≠ n₂ →
      Int.fract (↑((sigma k) n₁) / (↑n₁ ^ k : ℚ)) ≠
        Int.fract (↑((sigma k) n₂) / (↑n₂ ^ k : ℚ))

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

Sources

LeanOeisA1157.conjecture

TheoremPrime gaps #

Differences between consecutive primes: $a(n) = p_{n+1} - p_n$.

References: - A001223

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

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

`OeisA1223.conjecture`

Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/f02efd9a8c5fc6a735d2a90c33e24f7278ce0ffc/runs/oeis-full-50usd-oai-jajpvieznaevpoyg/prime_gap_subsequences_occur_infinitely_often/Submission/Spec.lean#L134.

Any subsequence a(n .. n+m) with n > 2 (as to exclude the untypical primes 2 and 3) should occur infinitely many times at other starting points k.

This is false. The five-term block starting at $n = 3$ is $(2,4,2,4,2)$, and a congruence modulo $5$ shows that it occurs only at $n = 3$.

theorem conjecture :
    ¬ ∀ (n m : ℕ), n ≥ 3 →
      Set.Infinite {k : ℕ | gapSubsequence k (m + 1) = gapSubsequence n (m + 1)}

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

Sources

LeanOeisA1223.conjecture

TheoremLesser of twin primes #

Primes $p$ such that $p+2$ is also prime.

References: - A001359

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

`OeisA1359.conjecture`

Solved: stated here; a Lean proof is at https://github.com/robzilla1738/formal-conjectures/blob/c7de1452e5b9b8165a30466637b83f7fedfb95fe/FormalConjectures/OEIS/1359.lean#L589.

Primes $p_k$ such that $p_k! \equiv 1 \pmod{p_{k+1}}$ with the exception of $p_{991} = 7841$ and other unknown primes $p_k$ for which $(p_k+1)(p_k+2)\cdots(p_{k+1}-2) \equiv 1 \pmod{p_{k+1}}$ where $p_{k+1} - p_k > 2$.

A formal proof is hosted at the formal_proof link: a Wilson-theorem argument with a fixed-divisor trial-division sieve and a verified length-7840 certificate.

theorem conjecture (k : ℕ) (hk : k > 1) :
    let Pk := Nat.nth Nat.Prime (k - 1)
    let Pk_succ := Nat.nth Nat.Prime k
    let Congruence := Pk.factorial ≡ 1 [MOD Pk_succ]
    let IsLesserTwinPrime := (Pk + 2).Prime
    let Wk_prod : ℕ := ∏ i ∈ Finset.Icc (Pk + 1) (Pk_succ - 2), i
    Congruence ↔ (IsLesserTwinPrime ∨ (k = 991) ∨ (Pk_succ - Pk > 2 ∧ Wk_prod ≡ 1 [MOD Pk_succ]))

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

Sources

LeanOeisA1359.conjecture

TheoremOre's harmonic numbers #

A001599 lists the positive integers whose positive divisors have an integral harmonic mean. Equivalently, $n$ belongs to the sequence when $\sigma_1(n) \mid n\sigma_0(n)$, where $\sigma_1(n)$ is the sum of the divisors of $n$ and $\sigma_0(n)$ is their number.

References: - A001599

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

`OeisA1599.eq_one_of_odd_of_a`

Open: stated without proof.

"Ore conjectured that 1 is the only odd harmonic number."

Reference: A001599

theorem eq_one_of_odd_of_a {n : ℕ} (hn : A n) (hodd : Odd n) : n = 1

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

Sources

LeanOeisA1599.eq_one_of_odd_of_a

TheoremSquares of double factorials #

Squares of double factorials: $a(n) = ((2n-1)!!)^2 = (1 \cdot 3 \cdot 5 \cdots (2n-1))^2$.

References: - A001818 - She, Sun, Xia, A novel permanent identity with applications, Theorem 1.3(ii) - Yang, Zhang, Sun-type determinant and permanent congruences, Proposition 17

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

`OeisA1818.conjecture1`

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

Conjecture 1: For any primitive $2n$-th root $\zeta$ of unity, the permanent of the $2n \times 2n$ matrix $[m(j,k)]_{j,k=1..2n}$ coincides with $a(n) = ((2n-1)!!)^2$, where $m(j,k)$ is $(1+\zeta^{j-k})/(1-\zeta^{j-k})$ if $j \neq k$, and $1$ otherwise. - Zhi-Wei Sun, Dec 21 2021

Proved by She, Sun and Xia, Theorem 1.3(ii) in the reference above. Lean formalization by Wentao Li, with AI assistance.

theorem conjecture1 (n : ℕ) (hn : 1 ≤ n) :
    ∀ (ζ : ℂ), IsPrimitiveRoot ζ (2 * n) →
      Matrix.permanent (fun (i j : Fin (2 * n)) =>
        if i = j then
          (1 : ℂ)
        else
          (1 + ζ ^ (i.val - j.val : ℤ)) / (1 - ζ ^ (i.val - j.val : ℤ))
      ) = (a n : ℂ)

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

`OeisA1818.conjecture2`

Solved: stated here without proof.

Conjecture 2: Let $p$ be an odd prime. Then the permanent of the $(p-1) \times (p-1)$ matrix $[f(j,k)]_{j,k=1..p-1}$ is congruent to $a((p-1)/2) = ((p-2)!!)^2 \pmod{p^2}$, where $f(j,k)$ is $(j+k)/(j-k)$ if $j \neq k$, and $f(j,k) = 1$ otherwise. - Zhi-Wei Sun, Dec 22 2021

theorem conjecture2 {p : ℕ} (hp : p.Prime) (h_odd : p ≠ 2) :
    let N : ℕ := p - 1
    let R := ZMod (p ^ 2)
    let Idx := Fin N
    let M : Matrix Idx Idx R := fun i j => fEntry (i.val + 1) (j.val + 1)
    (M.permanent : R) = (a ((p - 1) / 2) : R)

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

Sources

LeanOeisA1818.conjecture1 · OeisA1818.conjecture2

TheoremMultiplicative order of 2 mod $2n+1$#

The multiplicative order of 2 modulo $2n+1$. In other words, the least $m > 0$ such that $2n+1$ divides $2^m - 1$.

References: - A002326

Quoted from FormalConjectures/OEIS/2326.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 open. It also has 5 test statements, counted here but not shown.

`OeisA2326.conjecture1`

Open: stated without proof.

If $p$ is an odd prime then $a((p^3-1)/2) = p \cdot a((p^2-1)/2)$. Because otherwise $a((p^3-1)/2) < p \cdot a((p^2-1)/2)$ iff $a((p^3-1)/2) = a((p-1)/2)$ for a prime $p$. Equivalently $p^3$ divides $2^{p-1}-1$, but no such prime $p$ is known. - Thomas Ordowski, Feb 10 2014

theorem conjecture1 (p : ℕ) (hp : p.Prime) (hp_odd : p ≠ 2) :
    a ((p ^ 3 - 1) / 2) = p * a ((p ^ 2 - 1) / 2)

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

`OeisA2326.conjecture2`

Open: stated without proof.

A generalization of the previous conjecture: For each $k \ge 2$, if $p$ is an odd prime then $a((p^{k+1}-1)/2) = p \cdot a((p^k-1)/2)$. Computer testing of this generalized conjecture shows that there is no counterexample for $k$ and $p$ both up to 1000. - Ahmad J. Masad, Oct 17 2020

The two are in fact equivalent. Its $k = 2$ instance is conjecture1. Conversely, write $d = \operatorname{ord}_{p^2}(2)$. conjecture1 for $p$ says $v_p(2^d - 1) = 2$, and lifting the exponent for the odd prime $p$ then gives $v_p(2^{d p^t} - 1) = 2 + t$, hence $\operatorname{ord}_{p^{2+t}}(2) = d p^t$ for every $t \ge 0$, which is every instance for that $p$.

theorem conjecture2 (k : ℕ) (hk : 2 ≤ k) (p : ℕ) (hp : p.Prime) (hp_odd : p ≠ 2) :
    a ((p ^ (k + 1) - 1) / 2) = p * a ((p ^ k - 1) / 2)

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

Sources

LeanOeisA2326.conjecture1 · OeisA2326.conjecture2

TheoremCuban Primes #

OEIS A002407 lists the primes that are differences of two consecutive positive cubes. The sequence is conjectured to be infinite.

References: - OEIS A002407

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

`OeisA2407.conjecture`

Open: stated without proof.

This sequence is believed to be infinite.

theorem conjecture : {p : ℕ | A p}.Infinite

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

Sources

LeanOeisA2407.conjecture

TheoremCentral trinomial coefficients #

Central trinomial coefficients: largest coefficient of $(1 + x + x^2)^n$, which is the coefficient of $x^n$ in the expansion of $(1 + x + x^2)^n$.

References: - A002426

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

`OeisA2426.conjecture`

Open: stated without proof.

An integer $n > 3$ is prime if and only if $a(n) \equiv 1 \pmod{n^2}$. We have verified this for $n$ up to $8 \cdot 10^5$, and proved that $a(p) \equiv 1 \pmod{p^2}$ for any prime $p > 3$ (cf. A277640). - Zhi-Wei Sun, Nov 30 2016

theorem conjecture (n : ℕ) (hn : 3 < n) :
    n.Prime ↔ a n ≡ 1 [MOD n ^ 2]

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

Sources

LeanOeisA2426.conjecture

TheoremCentral factorial numbers: $((2n)!!)^2$#

Central factorial numbers: $a(n) = 4^n (n!)^2 = ((2n)!!)^2$.

References: - A002454 - [SSX22] She, Y.-F., Sun, Z.-W., Xia, W., A novel permanent identity with applications, arXiv:2208.12167 (2022)

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

`OeisA2454.conjecture`

Solved: stated here without proof.

Let $\zeta$ be a primitive $(2n+1)$-th root of unity. Then the permanent of the $2n \times 2n$ matrix $[m(j,k)]_{j,k=1..2n}$ is $a(n)/(2n+1) = ((2n)!!)^2/(2n+1)$, where $m(j,k)$ is $1$ or $(1+\zeta^{j-k})/(1-\zeta^{j-k})$ according as $j = k$ or not. - Zhi-Wei Sun, Jun 26 2022

Proved by [SSX22], Theorem 1.3(ii): for odd $m > 1$ and $\zeta$ a primitive $m$-th root of unity, the permanent of $[c_{j,k}]_{1 \le j,k \le m-1}$ is $((m-1)!!)^2/m$. Take $m = 2n+1$; translating both matrix indices by one leaves $j - k$ unchanged. For $n = 0$ the matrix is empty and both sides are $1$.

theorem conjecture (n : ℕ) :
    let N : ℕ := 2 * n
    let K : ℕ := N + 1
    ∀ (ζ : ℂ), IsPrimitiveRoot ζ K →
      Matrix.permanent (fun (j k : Fin N) =>
        if j = k then
          (1 : ℂ)
        else
          let pow : ℤ := (j : ℤ) - (k : ℤ)
          (1 + ζ ^ pow) / (1 - ζ ^ pow)
      ) = (a n : ℂ) / (K : ℂ)

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

Sources

LeanOeisA2454.conjecture

TheoremCoefficient of $(xyz)^n$ in $((x+y)(y+z)(z+x))^n$ equaling $\binom{2n}{n}^3$#

The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$.

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

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

`OeisA2897.a_eq_coeff`

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

Conjecture: $a(n) = [x^n y^n z^n] (1+x+y+z)^{2n} (1+x+y-z)^n (1+x-y+z)^n$. - Peter Bala, Apr 10 2022

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

theorem a_eq_coeff (n : ℕ) : (a n : ℤ) = MvPolynomial.coeff (xyzPowN n) (pPoly n)

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

Sources

LeanOeisA2897.a_eq_coeff

TheoremA binomial coefficient sum #

A binomial coefficient sum:

\[a(n) = \sum_{k=0}^{\lfloor n/2 \rfloor} \left( \binom{n}{k} - \binom{n}{k-1} \right)^3\]

where $\binom{n}{-1} = 0$.

References: - A003161 - [Li26] Wentao Li, A supercongruence for A003161, 2026.

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

`OeisA3161.conjecture`

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/41f7b2ba762827a74f1651e76a2ad6d77be6a021/LeanOeisProofs/NewFormalization/A003161.lean#L1717.

"Conjecture: Let $b(n) = a(2n-1)$. Then the supercongruence $b(np^k) \equiv b(np^{k-1}) \pmod{p^{3k}}$ holds for positive integers $n$ and $k$ and all primes $p \ge 5$." - Peter Bala, Mar 20 2023.

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

theorem conjecture (n k p : ℕ) (hn : 0 < n) (hk : 0 < k) (hp : p.Prime) (hp_ge : 5 ≤ p) :
    (b (n * p ^ k) : ℤ) ≡ (b (n * p ^ (k - 1)) : ℤ) [ZMOD (p : ℤ) ^ (3 * k)]

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

Sources

LeanOeisA3161.conjecture

TheoremA binomial coefficient summation #

A binomial coefficient summation: $a(n) = S(3, n) / S(1, n)$, where for a positive integer $r$ we define

\[S(r,n) = \sum_{k=0}^{\lfloor n/2 \rfloor} \left( \binom{n}{k} - \binom{n}{k-1} \right)^r\]

with $\binom{n}{-1} = 0$.

References: - A003162 - H. W. Gould, Problem E2384 (proposal), Amer. Math. Monthly, 81 (1974), 170-171 - [Li26] Wentao Li, A supercongruence for A003162, 2026.

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

`OeisA3162.a_is_integer`

Textbook result, stated without proof. A Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/41f7b2ba762827a74f1651e76a2ad6d77be6a021/LeanOeisProofs/NewFormalization/A003162.lean#L72.

$a(n)$ is an integer for all $n \ge 0$.

Gould proposed this as Monthly Problem E2384. The 1974 reference in the module docstring is that proposal, not a solution to it.

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

theorem a_is_integer (n : ℕ) : (a n).den = 1

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

`OeisA3162.conjecture`

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-oeis-proofs/blob/41f7b2ba762827a74f1651e76a2ad6d77be6a021/LeanOeisProofs/NewFormalization/A003162.lean#L115.

"Conjecture: Let $b(n) = a(2n-1)$. Then the supercongruence $b(np^k) \equiv b(np^{k-1}) \pmod{p^{3k}}$ holds for positive integers $n$ and $k$ and all primes $p \ge 5$." - Peter Bala, Mar 26 2023.

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

theorem conjecture (n k p : ℕ) (hn : 0 < n) (hk : 0 < k) (hp : p.Prime) (hp_ge : 5 ≤ p) :
    (b (n * p ^ k)).num ≡ (b (n * p ^ (k - 1))).num [ZMOD (p : ℤ) ^ (3 * k)]

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

Sources

LeanOeisA3162.a_is_integer · OeisA3162.conjecture

TheoremPrimes congruent to $\{3, 5, 6\} \pmod 7$#

Primes congruent to $3, 5, \text{ or } 6 \pmod 7$.

References: - A003625

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

`OeisA3625.conjecture`

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a003625-irreducibility/blob/d6c9f90827805142d81eee4e3d9099c8b48cbcc8/lean/OeisA3625FC.lean#L103-L104.

Conjecture: Represents primes $p$ where the polynomial $x^2 + x + 2$ is irreducible over $\text{GF}(p)$. - Federico Provvedi, Jul 21 2018

Answer: true, the equivalence is classical (complete the square: $4(x^2+x+2) = (2x+1)^2 + 7$, then use quadratic reciprocity).

theorem conjecture (p : ℕ) (hp : p.Prime) :
    A p ↔ Irreducible (X ^ 2 + X + 2 : (ZMod p)[X])

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

Sources

LeanOeisA3625.conjecture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Density of ones in the… to Primes congruent to ${3, 5…

TheoremDensity of ones in the Kolakoski sequence#

OeisA2.density_one

Sources

TheoremThe prime numbers#

OeisA40.conjecture

Sources

TheoremNo powers as partition numbers#

OeisA41.noPowerPartitionNumber

Sources

TheoremFractional parts of sums of reciprocals of Catalan numbers \(C(n)\)#

OeisA108.catalanReciprocalSum_fracPart_inj

Sources

TheoremNumber of squares \(\bmod n\)#

OeisA224.conjecture

Sources

TheoremEuclid-Mullin sequence#

OeisA945.every_prime_occurs

Sources

Theorem\(a(n) = 2^(2^n)\)#

OeisA1146.divisibility_fact

OeisA1146.conjecture

Sources

TheoremSum of squares of divisors of \(n\)#

OeisA1157.conjecture

Sources

TheoremPrime gaps#

OeisA1223.conjecture

Sources

TheoremLesser of twin primes#

OeisA1359.conjecture

Sources

TheoremOre's harmonic numbers#

OeisA1599.eq_one_of_odd_of_a

Sources

TheoremSquares of double factorials#

OeisA1818.conjecture1

OeisA1818.conjecture2

Sources

TheoremMultiplicative order of 2 mod \(2n+1\)#

OeisA2326.conjecture1

OeisA2326.conjecture2

Sources

TheoremCuban Primes#

OeisA2407.conjecture

Sources

TheoremCentral trinomial coefficients#

OeisA2426.conjecture

Sources

TheoremCentral factorial numbers: \(((2n)!!)^2\)#

OeisA2454.conjecture

Sources

TheoremCoefficient of \((xyz)^n\) in \(((x+y)(y+z)(z+x))^n\) equaling \(\binom{2n}{n}^3\)#

OeisA2897.a_eq_coeff

Sources

TheoremA binomial coefficient sum#

OeisA3161.conjecture

Sources

TheoremA binomial coefficient summation#

OeisA3162.a_is_integer

OeisA3162.conjecture

Sources

TheoremPrimes congruent to \(\{3, 5, 6\} \pmod 7\)#

OeisA3625.conjecture

Sources

TheoremDensity of ones in the Kolakoski sequence #

`OeisA2.density_one`

TheoremThe prime numbers #

`OeisA40.conjecture`

TheoremNo powers as partition numbers #

`OeisA41.noPowerPartitionNumber`

`OeisA108.catalanReciprocalSum_fracPart_inj`

`OeisA224.conjecture`

TheoremEuclid-Mullin sequence #

`OeisA945.every_prime_occurs`

`OeisA1146.divisibility_fact`

`OeisA1146.conjecture`

`OeisA1157.conjecture`

TheoremPrime gaps #

`OeisA1223.conjecture`

TheoremLesser of twin primes #

`OeisA1359.conjecture`

TheoremOre's harmonic numbers #

`OeisA1599.eq_one_of_odd_of_a`

TheoremSquares of double factorials #

`OeisA1818.conjecture1`

`OeisA1818.conjecture2`

`OeisA2326.conjecture1`

`OeisA2326.conjecture2`

TheoremCuban Primes #

`OeisA2407.conjecture`

TheoremCentral trinomial coefficients #

`OeisA2426.conjecture`

`OeisA2454.conjecture`

`OeisA2897.a_eq_coeff`

TheoremA binomial coefficient sum #

`OeisA3161.conjecture`

TheoremA binomial coefficient summation #

`OeisA3162.a_is_integer`

`OeisA3162.conjecture`

`OeisA3625.conjecture`