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.