Number of \(0 < k < n/2\) such… to Difference between \(n \tau(n)\)…
TheoremNumber of \(0 < k < n/2\) such that \(\phi(k)\phi(n-k)\) is a square#
Let \(\phi\) denote Euler's totient function. The sequence \(a(n)\) counts the number of integers \(0 < k < n/2\) such that \(\phi(k)\phi(n-k)\) is a square.
References: - A236998
Quoted from FormalConjectures/OEIS/236998.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 open. It also has 7 test statements, counted here but not shown.
OeisA236998.conjecture_1
Open: stated without proof.
Conjecture: (i) \(a(n) > 0\) for all \(n > 8\).
theorem conjecture_1 (n : ℕ) (hn : 8 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/236998.lean, line 64.
OeisA236998.conjecture_2
Open: stated without proof.
Conjecture: (ii) If \(n > 20\), then \(\phi(k)\phi(n-k) + 1\) is a square for some \(0 < k < n/2\).
theorem conjecture_2 (n : ℕ) (hn : 20 < n) :
∃ k : ℕ, 0 < k ∧ 2 * k < n ∧ IsSquare (k.totient * (n - k).totient + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/236998.lean, line 71.
OeisA236998.conjecture_3
Open: stated without proof.
Conjecture: (iii) If \(n > 1\) is not among \(4, 7, 60, 199, 267\), then \(k\phi(n-k)\) is a square for some \(0 < k < n\).
theorem conjecture_3 (n : ℕ) (hn : 1 < n) (h4 : n ≠ 4) (h7 : n ≠ 7) (h60 : n ≠ 60)
(h199 : n ≠ 199) (h267 : n ≠ 267) :
∃ k : ℕ, 0 < k ∧ k < n ∧ IsSquare (k * (n - k).totient)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/236998.lean, line 80.
Sources
TheoremNumber of parts in the symmetric representation of \(\sigma(n)\)#
Number of parts in the symmetric representation of \(\sigma(n)\). \(a(n)\) is \(1\) plus the number of pairs \((d_k, d_{k+1})\) of consecutive divisors of \(n\) such that \(d_{k+1}\) is odd and \(d_{k+1} \ge 2 d_k\).
The formula used is \(1 + |\{(d_k, d_{k+1}) \in \text{consecutive pairs of divisors of } n \mid d_{k+1} \text{ is odd and } d_{k+1} \ge 2 d_k\}|\), which is a known characterization of the sequence.
References: - A237271 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/237271.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 7 solved. It also has 5 test statements, counted here but not shown.
OeisA237271.conjecture_2
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/237271.wip.lean#L102.
Conjecture 2: "a(n) is the number of 2-dense sublists of divisors of n. We call '2-dense sublists of divisors of n' to the maximal sublists of divisors of n whose terms increase by a factor of at most 2." - Omar E. Pol, Jul 31 2025
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem conjecture_2 (n : ℕ) : a n = num2DenseSublists n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 116.
OeisA237271.conjecture_1
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA237271_conjecture_1.lean#L211.
Conjecture 1 / Theorem: "a(n) is the number of odd divisors of n except the 'e' odd divisors described in A005279." - Omar E. Pol, Dec 21 2024. "The conjecture 1 is true. For a proof see A379288." - Hartmut F. W. Hoft, Jan 21 2025. Equivalently, \(a(n) = \text{A001227}(n) - \text{A239657}(n)\). - Omar E. Pol, Mar 23 2014
theorem conjecture_1 (n : ℕ) (hn : 0 < n) :
a n = A001227 n - A239657 n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 134.
OeisA237271.a_odd_prime_pow
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA237271_a_odd_prime_pow.lean#L165.
Theorem: "a(p^k) = k + 1, where p is an odd prime and k >= 0." - Hartmut F. W. Hoft, Dec 26 2016
theorem a_odd_prime_pow (p k : ℕ) (hp : p.Prime) (ho : Odd p) :
a (p ^ k) = k + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 144.
OeisA237271.conjecture_3
Proved here.
Conjecture 3: "a(n) is the number of divisors p of n such that p is greater than twice the adjacent previous divisor of n. The divisors p give the n-th row of A379288." - Omar E. Pol, Aug 02 2025
Note: this is equivalent to
a_eq_num2DenseSublists(Conjecture 2), since the divisors that start a new 2-dense sublist are exactly those greater than twice their predecessor (plus the smallest divisor).
theorem conjecture_3 (n : ℕ) :
a n = 1 + ((sortedDivisorsList n).zip (sortedDivisorsList n).tail).countP
fun pair => pair.snd > 2 * pair.fst
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 158.
OeisA237271.conjecture_4
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a237271-square-hexagonal-parity/blob/430c09114d4ad3a3a2654b9816c8bfdc3cdf38de/lean/OeisA237271ParityFC.lean#L19-L24.
Conjecture 4: "a(A000290(n)) is odd." - Omar E. Pol, Oct 21 2025
That is, the number of parts in the symmetric representation of \(\sigma(n^2)\) is always odd.
theorem conjecture_4 (n : ℕ) (hn : 0 < n) : Odd (a (n ^ 2))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 172.
OeisA237271.conjecture_5
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a237271-square-hexagonal-parity/blob/430c09114d4ad3a3a2654b9816c8bfdc3cdf38de/lean/OeisA237271ParityFC.lean#L26-L32.
Conjecture 5: "a(A000384(n)) is odd." - Omar E. Pol, Oct 21 2025
That is, the number of parts in the symmetric representation of \(\sigma(n(2n-1))\) is always odd, where \(n(2n-1)\) is the \(n\)-th hexagonal number.
theorem conjecture_5 (n : ℕ) (hn : 0 < n) : Odd (a (n * (2 * n - 1)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 185.
OeisA237271.observation_carmichael
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_OeisA237271_observation_carmichael.lean#L260.
Observation: "a(A002997(n)) >= 3, at least for 1 <= n <= 10000." - Omar E. Pol, Oct 21 2025
That is, \(a(k) \ge 3\) for every Carmichael number \(k\). A002997 is the sequence of Carmichael numbers: the composite numbers \(k\) such that \(b^{k-1} \equiv 1 \pmod k\) for every \(b\) coprime to \(k\). This is
IsCarmichael, which also forces \(k\) to be composite.The observation holds for every odd composite \(k\), so in particular for every Carmichael number. Write \(p\) for the least prime factor of \(k\) and \(q = k/p\). The two smallest divisors of \(k\) are \(1\) and \(p\), and the two largest are \(q\) and \(k\), so \((1, p)\) and \((q, k)\) are both consecutive pairs in the sorted divisor list, and they are distinct because \(1 < q\). Both qualify: \(p\) and \(k\) are odd, \(p \ge 2 \cdot 1\), and \(k = pq \ge 3q > 2q\). Hence the count is at least \(2\) and \(a(k) \ge 3\). A Carmichael number is odd: it is composite by the \(b = 1\) case of
IsCarmichael, so \(k > 2\), and if \(k\) were even then the coprime base \(k - 1 \equiv -1\) would give \(k \mid (-1)^{k-1} - 1 = -2\).
theorem observation_carmichael (k : ℕ) (hk : IsCarmichael k) :
3 ≤ a k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237271.lean, line 208.
Sources
TheoremOrdered ways to write \(n = k + m\) with \(p_k + 4\) and \(p_{p_m} + 4\) both prime#
Let \(p_j\) denote the \(j\)-th prime number. The sequence \(a(n)\) counts the number of ordered ways to write \(n = k + m\) with \(k > 0\) and \(m > 0\) such that \(p_k + 4\) and \(p_{p_m} + 4\) are both prime.
References: - A237348
Quoted from FormalConjectures/OEIS/237348.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.
OeisA237348.conjecture_1
Open: stated without proof.
Conjecture: For each \(d = 1, 2, 3, \dots\) there is a positive integer \(N(d)\) for which any integer \(n > N(d)\) can be written as \(k + m\) with \(k > 0\) and \(m > 0\) such that \(p_k + 2d\) and \(p_{p_m} + 2d\) are both prime.
theorem conjecture_1 (d : ℕ) (hd : 1 ≤ d) :
∃ N : ℕ, 0 < N ∧ ∀ n : ℕ, N < n →
∃ k m : ℕ, 0 < k ∧ 0 < m ∧ n = k + m ∧
(Nat.nth Nat.Prime (k - 1) + 2 * d).Prime ∧
(Nat.nth Nat.Prime (Nat.nth Nat.Prime (m - 1) - 1) + 2 * d).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237348.lean, line 83.
OeisA237348.conjecture_2
Open: stated without proof.
In particular, we may take \((N(1), N(2), \dots, N(10)) = (2, 11, 4, 15, 31, 4, 2, 77, 4, 7)\) in the conjecture.
theorem conjecture_2 (d : Fin 10) (n : ℕ)
(hn : ![2, 11, 4, 15, 31, 4, 2, 77, 4, 7] d < n) :
∃ k m : ℕ, 0 < k ∧ 0 < m ∧ n = k + m ∧
(Nat.nth Nat.Prime (k - 1) + 2 * (d.val + 1)).Prime ∧
(Nat.nth Nat.Prime (Nat.nth Nat.Prime (m - 1) - 1) + 2 * (d.val + 1)).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237348.lean, line 95.
Sources
TheoremWays to write \(n = k + m\) with \(p_k^2 - 2\), \(p_m^2 - 2\), and \(p_{p_m}^2 - 2\) all prime#
Let \(p_j\) denote the \(j\)-th prime number. The sequence \(a(n)\) counts the number of ways to write \(n = k + m\) with \(k > 0\) and \(m > 0\) such that \(p_k^2 - 2\), \(p_m^2 - 2\), and \(p_{p_m}^2 - 2\) are all prime.
References: - A237413
Quoted from FormalConjectures/OEIS/237413.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.
OeisA237413.conjecture
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture (n : ℕ) (hn : 1 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237413.lean, line 86.
Sources
TheoremNumber of \(0 < k < n\) such that \(\pi(kn)\) is prime#
Let \(\pi\) denote the prime counting function. The sequence \(a(n)\) counts the number of integers \(0 < k < n\) such that \(\pi(kn)\) is prime.
References: - A237578
Quoted from FormalConjectures/OEIS/237578.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 open. It also has 5 test statements, counted here but not shown.
OeisA237578.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 2\).
theorem conjecture_1 (n : ℕ) (hn : 2 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237578.lean, line 58.
OeisA237578.conjecture_2
Open: stated without proof.
and \(a(n) = 1\) only for \(n = 5, 8, 13\).
theorem conjecture_2 (n : ℕ) :
a n = 1 ↔ n = 5 ∨ n = 8 ∨ n = 13
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237578.lean, line 65.
OeisA237578.conjecture_3
Open: stated without proof.
Moreover, for each \(n = 1, 2, 3, \dots\), there is a positive integer \(k < 3\sqrt{n} + 3\) with \(\pi(kn)\) prime.
theorem conjecture_3 (n : ℕ) (hn : 1 ≤ n) :
∃ k : ℕ, 0 < k ∧ (k : ℝ) < 3 * Real.sqrt (n : ℝ) + 3 ∧
(Nat.primeCounting (k * n)).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237578.lean, line 74.
Sources
TheoremNumber of primes \(p \le (n+1)/2\) with \(\lfloor\sqrt{n-p}\rfloor\) prime#
The sequence \(a(n)\) counts the number of primes \(p \le \lfloor (n+1)/2 \rfloor\) such that \(\lfloor\sqrt{n-p}\rfloor\) is prime.
References: - A237720
Quoted from FormalConjectures/OEIS/237720.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 open. It also has 7 test statements, counted here but not shown.
OeisA237720.conjecture_1
Open: stated without proof.
Conjecture (i): \(a(n) > 0\) for all \(n > 5\).
theorem conjecture_1 (n : ℕ) (hn : 5 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237720.lean, line 65.
OeisA237720.conjecture_2
Open: stated without proof.
Conjecture: \(a(n) = 1\) only for \(n = 6, 23, 24, 111, 112, \ldots, 120\).
theorem conjecture_2 (n : ℕ) :
a n = 1 ↔ n = 6 ∨ n = 23 ∨ n = 24 ∨ (111 ≤ n ∧ n ≤ 120)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237720.lean, line 72.
OeisA237720.conjecture_3
Open: stated without proof.
Conjecture (ii): For any integer \(n > 2\), there is a prime \(p < n\) with \(\lfloor\sqrt{n+p}\rfloor\) prime.
theorem conjecture_3 (n : ℕ) (hn : 2 < n) :
∃ p : ℕ, p.Prime ∧ p < n ∧ (Nat.sqrt (n + p)).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/237720.lean, line 81.
Sources
TheoremPairs \(\{j, k\}\) with \(0 < j < k \le n\), \(k \equiv 1 \pmod j\), and \(\pi(jn) \mid \pi(kn)\)#
Let \(\pi\) denote the prime counting function. The sequence \(a(n)\) counts the number of pairs \((j, k)\) with \(0 < j < k \le n\) and \(k \equiv 1 \pmod j\) such that \(\pi(jn)\) divides \(\pi(kn)\).
References: - A238224
Quoted from FormalConjectures/OEIS/238224.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.
OeisA238224.conjecture
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 1\).
theorem conjecture (n : ℕ) (hn : 1 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238224.lean, line 61.
Sources
TheoremEqual prime counts in adjacent intervals \((kn, (k+1)n)\) and \(((k+1)n, (k+2)n)\)#
Let \(\pi\) denote the prime counting function. The sequence \(a(n)\) counts the number of integers \(0 < k < n\) such that the intervals \((kn, (k+1)n)\) and \(((k+1)n, (k+2)n)\) contain the same number of primes.
References: - A238281
Quoted from FormalConjectures/OEIS/238281.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 open. It also has 5 test statements, counted here but not shown.
OeisA238281.conjecture_1
Open: stated without proof.
Conjecture (i): \(a(n) > 0\) for all \(n > 1\).
theorem conjecture_1 (n : ℕ) (hn : 1 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238281.lean, line 61.
OeisA238281.conjecture_2
Open: stated without proof.
Conjecture: Moreover, if \(n > 1\) is not equal to \(8\), then there is a positive integer \(k < n\) with \(2k + 1\) prime such that the two intervals \(((k-1)n, kn]\) and \((kn, (k+1)n]\) contain the same number of primes.
OEIS states open intervals, but for \(n = 2\) the only candidate is \(k = 1\), where the open interval \((0, 2)\) contains 0 primes while \((2, 4)\) contains 1 prime. Half-open intervals \(((k-1)n, kn]\) match Sun's Mathematica formula
PrimePi[k*n] - PrimePi[(k-1)*n]and hold for \(n = 2\).
theorem conjecture_2 (n : ℕ) (hn : 1 < n) (h8 : n ≠ 8) :
∃ k : ℕ, 0 < k ∧ k < n ∧ (2 * k + 1).Prime ∧
Nat.primeCounting (k * n) - Nat.primeCounting ((k - 1) * n) =
Nat.primeCounting ((k + 1) * n) - Nat.primeCounting (k * n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238281.lean, line 75.
OeisA238281.conjecture_3
Open: stated without proof.
Conjecture (ii): For any integer \(n > 4\), there is a positive integer \(k < p_n\) such that all the three intervals \((kn, (k+1)n)\), \(((k+1)n, (k+2)n)\), \(((k+2)n, (k+3)n)\) contain the same number of primes, i.e., \(\pi(kn)\), \(\pi((k+1)n)\), \(\pi((k+2)n)\), \(\pi((k+3)n)\) form a \(4\)-term arithmetic progression.
theorem conjecture_3 (n : ℕ) (hn : 4 < n) :
∃ k : ℕ, 0 < k ∧ k < Nat.nth Nat.Prime (n - 1) ∧
Nat.primeCounting ((k + 1) * n) - Nat.primeCounting (k * n) =
Nat.primeCounting ((k + 2) * n) - Nat.primeCounting ((k + 1) * n) ∧
Nat.primeCounting ((k + 2) * n) - Nat.primeCounting ((k + 1) * n) =
Nat.primeCounting ((k + 3) * n) - Nat.primeCounting ((k + 2) * n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238281.lean, line 88.
Sources
TheoremNumber of positive integers \(k < n\) such that \(n^2 - \pi(k n)\) is prime#
The sequence \(a(n)\) counts the number of positive integers \(k < n\) such that \(n^2 - \pi(k n)\) is prime, where \(\pi(x)\) is the prime counting function:
\[a(n) = |\{0 < k < n : n^2 - \pi(k n) \text{ is prime}\}|\]References: - A238568 - Problems on combinatorial properties of primes by Zhi-Wei Sun (2014)
Quoted from FormalConjectures/OEIS/238568.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 5 open. It also has 5 test statements, counted here but not shown.
OeisA238568.conjecture_1
Open: stated without proof.
Conjecture (i): \(a(n) > 0\) for all \(n > 1\).
theorem conjecture_1 (n : ℕ) (hn : 1 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238568.lean, line 67.
OeisA238568.conjecture_2
Open: stated without proof.
Conjecture (i): \(a(n) = 1\) only for \(n \in \{2, 3, 4, 8, 10, 24, 41\}\).
theorem conjecture_2 (n : ℕ) :
a n = 1 ↔ n ∈ ({2, 3, 4, 8, 10, 24, 41} : Set ℕ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238568.lean, line 74.
OeisA238568.conjecture_3
Open: stated without proof.
Conjecture (ii): For any integer \(n > 6\), there is a positive integer \(k < n\) with \(n^2 + \pi(k n) - 1\) prime.
theorem conjecture_3 (n : ℕ) (hn : 6 < n) :
∃ k : ℕ, 0 < k ∧ k < n ∧ Nat.Prime (n ^ 2 + Nat.primeCounting (k * n) - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238568.lean, line 83.
OeisA238568.conjecture_4
Open: stated without proof.
Conjecture (iii), part 1: If \(n > 2\), then \(\pi(n^2) - \pi(k n)\) is prime for some \(0 < k < n\).
theorem conjecture_4 (n : ℕ) (hn : 2 < n) :
∃ k : ℕ, 0 < k ∧ k < n ∧
Nat.Prime (Nat.primeCounting (n ^ 2) - Nat.primeCounting (k * n))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238568.lean, line 91.
OeisA238568.conjecture_5
Open: stated without proof.
Conjecture (iii), part 2: If \(n > 1\), then \(\pi(n^2) + \pi(k n) - 1\) is prime for some \(0 < k < n\).
theorem conjecture_5 (n : ℕ) (hn : 1 < n) :
∃ k : ℕ, 0 < k ∧ k < n ∧
Nat.Prime (Nat.primeCounting (n ^ 2) + Nat.primeCounting (k * n) - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238568.lean, line 100.
Sources
TheoremNumber of primes \(p < n\) with \(\text{prime}(p)^2 + (\text{prime}(n) - 1)^2\) prime#
The sequence \(a(n)\) counts the number of primes \(p < n\) such that \(\text{prime}(p)^2 + (\text{prime}(n) - 1)^2\) is prime, where \(\text{prime}(i)\) denotes the \(i\)-th prime number (1-indexed).
References: - A238585 - Problems on combinatorial properties of primes by Zhi-Wei Sun (2014)
Quoted from FormalConjectures/OEIS/238585.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 5 open. It also has 6 test statements, counted here but not shown.
OeisA238585.conjecture_1
Open: stated without proof.
Conjecture (i): \(a(n) > 0\) unless \(n\) divides \(6\).
theorem conjecture_1 (n : ℕ) (hn : 0 < n) :
0 < a n ↔ ¬(n ∣ 6)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238585.lean, line 95.
OeisA238585.conjecture_2
Open: stated without proof.
Conjecture (i): \(a(n) = 1\) only for \(n \in \{4, 5, 7, 10, 11, 12, 19, 21, 22, 31, 42, 44\}\).
theorem conjecture_2 (n : ℕ) (hn : 0 < n) :
a n = 1 ↔ n ∈ ({4, 5, 7, 10, 11, 12, 19, 21, 22, 31, 42, 44} : Set ℕ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238585.lean, line 104.
OeisA238585.conjecture_3
Open: stated without proof.
Conjecture (ii): If \(n > 2\) is not equal to \(9\), then \(\text{prime}(n)^2 + (\text{prime}(p) - 1)^2\) is prime for some prime \(p < n\).
theorem conjecture_3 (n : ℕ) (hn : 2 < n) (hn9 : n ≠ 9) :
∃ p : ℕ, p < n ∧ p.Prime ∧
Nat.Prime (Nat.nth Nat.Prime (n - 1) ^ 2 + (Nat.nth Nat.Prime (p - 1) - 1) ^ 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238585.lean, line 113.
OeisA238585.conjecture_4
Open: stated without proof.
Conjecture (iii), part 1: For \(n > 3\), there is a prime \(p < n\) with \(\text{prime}(p) + \text{prime}(n) + 1\) prime.
theorem conjecture_4 (n : ℕ) (hn : 3 < n) :
∃ p : ℕ, p < n ∧ p.Prime ∧
Nat.Prime (Nat.nth Nat.Prime (p - 1) + Nat.nth Nat.Prime (n - 1) + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238585.lean, line 123.
OeisA238585.conjecture_5
Open: stated without proof.
Conjecture (iii), part 2: If \(n > 9\) is not equal to \(18\), then \(\text{prime}(p)^2 + \text{prime}(n)^2 - 1\) is prime for some prime \(p < n\).
theorem conjecture_5 (n : ℕ) (hn : 9 < n) (hn18 : n ≠ 18) :
∃ p : ℕ, p < n ∧ p.Prime ∧
Nat.Prime (Nat.nth Nat.Prime (p - 1) ^ 2 + Nat.nth Nat.Prime (n - 1) ^ 2 - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238585.lean, line 133.
Sources
TheoremNumber of integers \(0 < k \le n\) such that \(\pi(\pi(k n))\) is a square#
The sequence \(a(n)\) counts the number of integers \(k \in \{1, \dots, n\}\) such that \(\pi(\pi(k n))\) is a square, where \(\pi(x)\) is the prime counting function:
\[a(n) = |\{0 < k \le n : \pi(\pi(k n)) \text{ is a square}\}|\]References: - A238902 - Problems on combinatorial properties of primes by Zhi-Wei Sun (2014)
Quoted from FormalConjectures/OEIS/238902.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.
OeisA238902.conjecture_1
Open: stated without proof.
Conjecture (i): \(a(n) > 0\) for all \(n > 0\).
theorem conjecture_1 (n : ℕ) (hn : 0 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238902.lean, line 69.
OeisA238902.conjecture_2
Open: stated without proof.
Conjecture (ii): For every \(n = 1, 2, 3, \dots\), there exists a positive integer \(k \le (n + 1) / 2\) such that \(\pi(\pi(k n))\) is a triangular number.
theorem conjecture_2 (n : ℕ) (hn : 0 < n) :
∃ k : ℕ, 0 < k ∧ k ≤ (n + 1) / 2 ∧
(Nat.primeCounting (Nat.primeCounting (k * n))).IsTriangular
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/238902.lean, line 77.
Sources
TheoremPrimitive roots of the form k² + 1#
Every prime \(p\) has a primitive root \(0 < g < p\) of the form \(k^2 + 1\), where \(k\) is an integer.
Zhi-Wei Sun has offered a prize of RMB 2,000 for the first proof.
References: - A239957 - Z.-W. Sun, "New observations on primitive roots modulo primes," arXiv:1405.0290 [math.NT], 2014.
Quoted from FormalConjectures/OEIS/239957.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 1 test statement, counted here but not shown.
OeisA239957.conjecture
Open: stated without proof.
Zhi-Wei Sun's Conjecture (A239957): Every prime \(p\) has a primitive root \(0 < g < p\) of the form \(k^2 + 1\), where \(k\) is an integer.
theorem conjecture (p : ℕ) (hp : p.Prime) : A p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/239957.lean, line 49.
Sources
TheoremWays of writing \(n\) as an ordered sum of a triangular, square, and pentagonal number#
The sequence \(a(n)\) counts the number of tuples \((i, j, k) \in \mathbb{N}^3\) such that \(T_i + S_j + P_k = n\), where \(T_i = i(i+1)/2\), \(S_j = j^2\), and \(P_k = k(3k-1)/2\):
\[a(n) = |\{(i, j, k) \in \mathbb{N}^3 : i(i+1)/2 + j^2 + k(3k-1)/2 = n\}|\]References: - A240088 - On universal sums of polygonal numbers by Zhi-Wei Sun, Sci. China Math. 58 (2015), 1367–1396.
Quoted from FormalConjectures/OEIS/240088.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.
OeisA240088.conjecture
Open: stated without proof.
It is conjectured that \(a(n)\) is always positive (Conjecture 1.1 of Sun (2009)).
theorem conjecture (n : ℕ) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/240088.lean, line 69.
Sources
TheoremLargest smallest-base in a decomposition of \(n\) into at most four squares#
The sequence \(a(n)\) is the largest integer \(k\) such that \(n = k^2 + \dots\) is a decomposition of \(n\) into a sum of at most four nondecreasing squares:
\[a(n) = \max \{k \ge 1 : \exists b_1, b_2, b_3 \in \{0\} \cup [k, n], k^2 + b_1^2 + b_2^2 + b_3^2 = n\}\]References: - A241898
Quoted from FormalConjectures/OEIS/241898.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 5 test statements, counted here but not shown.
OeisA241898.conjecture_1
Solved: stated here without proof.
"From the data that I have, it would seem that \(a(n)\) is greater than \(7\) for all \(n > 599\)." - David S. Newman, May 02 2014
This is false: since every four-square decomposition of a multiple of \(8\) uses only even squares, \(a(4m) = 2a(m)\) for all even \(m \ge 2\). From \(a(46) = 1\) (via \(46 = 1^2 + 3^2 + 6^2\)) we obtain \(a(184) = 2\) and \(a(736) = a(16 \cdot 46) = 4 \le 7\).
theorem conjecture_1 : ¬ ∀ n : ℕ, 599 < n → 7 < a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/241898.lean, line 79.
OeisA241898.conjecture_2
Open: stated without proof.
"By Lagrange's Theorem every number can be written as a sum of four squares. Can the same be said of the set of \(\{a^2 \mid a \text{ is any integer not equal to } 7\}\)? If this could be proved, it would only remain to check if all the numbers up to \(599\) can be written as the sum of \(4\) squares none of which is \(7^2\)." - David S. Newman, May 02 2014
Note that \(0 \in \mathbb{N} \setminus \{7\}\) allows representations as a sum of at most four positive squares none of which is \(7^2\).
theorem conjecture_2 :
∀ n : ℕ, ∃ a b c d : ℕ,
a ≠ 7 ∧ b ≠ 7 ∧ c ≠ 7 ∧ d ≠ 7 ∧ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/241898.lean, line 93.
Sources
TheoremLeast primitive prime divisor of the Franel numbers of order \(4\)#
Let \(f_r(n) = \sum_{k=0}^n \binom{n}{k}^r\) be the Franel number of order \(r\). The sequence \(a(n)\) is the least prime divisor of \(f_4(n)\) (A005260) that does not divide any previous term \(f_4(k)\) with \(1 \le k < n\), or \(1\) if no such prime divisor exists.
References: - A242174
Quoted from FormalConjectures/OEIS/242174.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.
OeisA242174.conjecture_1
Open: stated without proof.
Conjecture: \(a(n)\) is prime for any \(n > 0\).
theorem conjecture_1 (n : ℕ) (hn : 0 < n) : (a n).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/242174.lean, line 77.
OeisA242174.conjecture_2
Open: stated without proof.
"In general, for any \(r > 2\), if \(n\) is large enough then \(f_r(n) = \sum_{k=0}^n \binom{n}{k}^r\) has a prime divisor which does not divide any previous terms \(f_r(k)\) with \(k < n\)."
theorem conjecture_2 (r : ℕ) (hr : 2 < r) :
∃ N : ℕ, ∀ n : ℕ, N ≤ n → primitivePrimeDivisorFranel r n ≠ 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/242174.lean, line 85.
Sources
TheoremSmallest \(k \ge 1\) such that the concatenation of \(k\) threes and \(\text{prime}(n)\) is prime#
Let \(b_k = 3 \dots 3\) consist of \(k \ge 1\) threes in base \(10\). The sequence \(a(n)\) is the smallest \(k \ge 1\) such that the decimal concatenation of \(b_k\) and \(\text{prime}(n)\) is prime, or \(a(n) = 0\) if no such prime exists.
References: - A242775
Quoted from FormalConjectures/OEIS/242775.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.
OeisA242775.conjecture
Open: stated without proof.
Conjecture: For \(n \ge 4\), \(a(n) > 0\).
theorem conjecture (n : ℕ) (hn : 4 ≤ n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/242775.lean, line 155.
Sources
TheoremSigned digit sums in bases \(b \ge 5\)#
The sequence is defined by
\[a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k\]where the sign is \(-1\) if \(k\) is prime, and \(1\) if \(k\) is not prime.
Generalizing the digit pattern observed in \(a(n)\), it was conjectured on the OEIS entry that for any base \(b \ge 5\) and any choice of signs \(\pm 1\), the absolute value of \(\sum_{k=1}^n \pm b^k\) only contains digits in \(\{0, 1, b-2, b-1\}\).
References: - A243106 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/243106.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.
OeisA243106.digits_sum_restricted
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/243106.wip.lean#L140.
Conjecture: When expressed in base \(b \ge 5\), the absolute value of any partial sum \(\sum \pm b^k\) only contains digits belonging to \(\{0, 1, b-2, b-1\}\).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem digits_sum_restricted (b n : ℕ) (hb : b ≥ 5) :
∀ (σ : ℕ → Int) (hσ : ∀ k ∈ Icc 1 n, σ k = 1 ∨ σ k = -1),
let x : Int := (Icc 1 n).sum fun k ↦ σ k * (b : Int) ^ k;
∀ d ∈ (b.digits x.natAbs), d = 0 ∨ d = 1 ∨ d = b - 2 ∨ d = b - 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/243106.lean, line 78.
Sources
TheoremLeast index \(i\) for which \(\text{num}(\sigma_1(i)/i) - \text{den}(\sigma_1(i)/i) = n\)#
Let \(A243473(i)\) be the difference between the numerator \(p\) and the denominator \(q\) when the abundancy index \(\sigma_1(i) / i\) is written in lowest terms \(p / q\). The sequence \(a(n)\) is the least positive integer \(i\) such that \(A243473(i) = n\), or \(0\) if no such index exists.
References: - A243512
Quoted from FormalConjectures/OEIS/243512.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.
OeisA243512.conjecture
Open: stated without proof.
Motivated by the observation that some small numbers \((2, 12, 14, 18, \dots)\) occur only very late in the recently added sequence A243473, but all numbers seem to appear sooner or later. (The definition is completed by "\(0\) if no such index exists" to guarantee well-definedness in absence of a proof, but I conjecture that no such \(0\) will ever occur.)
theorem conjecture (n : ℕ) : a n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/243512.lean, line 76.
Sources
TheoremSum of \(d \cdot \tau(d)\) over proper divisors \(d\) of \(n\)#
The sequence \(a(n)\) is the sum of \(d \cdot \tau(d)\) over all proper divisors \(d < n\) of \(n\), where \(\tau(d)\) is the number of divisors of \(d\):
\[a(n) = \sum_{d \mid n, d < n} d \cdot \tau(d)\]References: - A245211
Quoted from FormalConjectures/OEIS/245211.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.
OeisA245211.conjecture
Open: stated without proof.
Conjecture: \(21\) is the only positive integer \(n\) such that \(a(n) = n\).
theorem conjecture (n : ℕ) (hn : 0 < n) : a n = n ↔ n = 21
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/245211.lean, line 66.
Sources
TheoremDifference between \(n \tau(n)\) and \(\sum_{d \mid n, d < n} d \tau(d)\)#
The sequence \(a(n) = n \tau(n) - \sum_{d \mid n, d < n} d \tau(d)\), where \(\tau(n)\) is the number of divisors of \(n\).
References: - A245212
Quoted from FormalConjectures/OEIS/245212.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.
OeisA245212.conjecture
Open: stated without proof.
Conjecture: \(a(n) = \sigma(n)\) iff \(n\) is a power of \(2\) (A000079).
theorem conjecture (n : ℕ) (h : 0 < n) :
a n = (σ 1 n : ℤ) ↔ ∃ k : ℕ, n = 2 ^ k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/245212.lean, line 59.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.