Least positive multiple of \(n\)… to Number of primes \(< n^2\)
TheoremLeast positive multiple of \(n\) in base 10 with digits 0 and 1#
Least positive multiple of \(n\) that when written in base 10 uses only 0's and 1's.
References: - A004290
Quoted from FormalConjectures/OEIS/4290.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 textbook result. It also has 3 test statements, counted here but not shown.
OeisA4290.a_ten_pow
Textbook result, proved here.
\(a(10^k) = 10^k\) for all \(k\).
theorem a_ten_pow (k : ℕ) : a (10 ^ k) = 10 ^ k
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OEIS/4290.lean, line 109.
OeisA4290.conjecture
Open: stated without proof.
It is known that \(a(10^k - 1) = (10^{9k} - 1) / 9\) for all \(k\). Is \(a(n) < a(10^k - 1)\) for all \(n < 10^k - 1\)? - David Radcliffe, Aug 01 2025
theorem conjecture (k : ℕ) :
∀ n < 10 ^ k - 1, a n < a (10 ^ k - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/4290.lean, line 129.
Sources
TheoremRecamán's sequence#
Start with \(a(0)=0\). At step \(n>0\), subtract \(n\) from the preceding term when the result is nonnegative and has not appeared earlier; otherwise add \(n\).
References: - OEIS A005132
Quoted from FormalConjectures/OEIS/5132.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 10 test statements and 7 API statements, counted here but not shown.
OeisA5132.conjecture
Open: stated without proof.
“I conjecture that every number eventually appears” — N. J. A. Sloane, OEIS A005132.
Sloane later added that he was no longer sure every number appears. The coverage question remains open and is formalized here as surjectivity onto the natural numbers.
theorem conjecture : Function.Surjective a
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/5132.lean, line 168.
Sources
TheoremPractical numbers#
A positive integer \(n\) is called a practical number (or panarithmic number) if every positive integer \(m \le n\) can be represented as a sum of distinct divisors of \(n\).
References: - A005153
Quoted from FormalConjectures/OEIS/5153.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.
OeisA5153.conjecture
Open: stated without proof.
Conjecture: every odd number, beginning with 3, is the sum of a prime number and a practical number. - Hal M. Switkay, Jan 28 2023
theorem conjecture (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) :
∃ p q : ℕ, p.Prime ∧ A q ∧ n = p + q
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/5153.lean, line 104.
Sources
TheoremApéry numbers#
Apéry numbers:
\[a(n) = \sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}\]References: - A005258
Quoted from FormalConjectures/OEIS/5258.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.
OeisA5258.conjecture
Open: stated without proof.
For each \(n = 1, 2, 3, \dots\) the polynomial \(a_n(x) = \sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k} x^k\) is irreducible over the field of rational numbers. - Zhi-Wei Sun, Mar 21 2013
theorem conjecture (n : ℕ) (hn : 1 ≤ n) : Irreducible (aperyPoly n)
Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/OEIS/5258.lean, line 67.
Sources
TheoremSubword complexity of the morphism a → aab, b → b#
Let \(a_n\) be the number of distinct subwords (contiguous factors) of length \(n\) in the infinite word generated by the morphism \(\sigma: a \mapsto aab, b \mapsto b\), starting from \(a\). As shown in the references, \(a_n\) is given by the formula
\[ a_n = \sum_{i=0}^{n} \min(2^i,n-i+1). \]The conjectured generating function is:
\[\sum_{n \geq 0} a_n x^n = \frac{1}{1-x} + \frac{x}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 1} x^{2^k + k - 1}\right).\]References: - A6697 - J.-P. Allouche and J. Shallit, "On the subword complexity of the fixed point of a → aab, b → b, and generalizations," arXiv:1605.02361 [math.CO], 2016. - N. J. A. Sloane and Simon Plouffe, The Encyclopedia of Integer Sequences, Academic Press, 1995.
Quoted from FormalConjectures/OEIS/6697.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 API statements, counted here but not shown.
OeisA6697.conjecture
Solved: stated here; a Lean proof is at https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/OeisA6697/solution.lean.
Conjecture (A6697): The generating function for the number of subwords of length \(n\) in the infinite word generated by \(a \mapsto aab, b \mapsto b\) is
\[\sum_{n \geq 0} a_n x^n = 1 + \frac{1}{1-x} + \frac{1}{(1-x)^2}\left(\frac{1}{1-x} - \sum_{k \geq 0} x^{2^{k+1} + k}\right).\]Equivalently, a(n) equals the n-th coefficient of this generating function.
However, the reference quoted in the OEIS sequence
J.-P. Allouche and J. Shallit, "On the subword complexity of the fixed point of a → aab, b → b, and generalizations," arXiv:1605.02361 [math.CO], 2016.
provides an explicit formula
\[ a_n = \sum_{i=0}^{n} \min(2^i,n-i+1). \]If one takes this as a definition of a(n) instead, it becomes straightforward to prove the conjecture. See https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/docs/OeisA6697.md for a formal proof of the generating function using this definition.
Hence, a formalization of arXiv:1605.02361 would complete a formal proof as below.
theorem conjecture (n : ℕ) :
a n = coeff (R := ℚ) n
((1 - X)⁻¹ + X * (1 - X)⁻¹ ^ 2 * ((1 - X)⁻¹ - ∑' k, X ^ (2 ^ (k + 1) + k)))
Category research solved; AMS 68 Computer science. Declared in FormalConjectures/OEIS/6697.lean, line 125.
Sources
TheoremCatalan-Mersenne numbers#
Catalan-Mersenne numbers: \(a(0) = 2\); for \(n \ge 0\), \(a(n+1) = 2^{a(n)} - 1\).
References: - A007013
Quoted from FormalConjectures/OEIS/7013.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.
OeisA7013.conjecture
Open: stated without proof.
Catalan-Mersenne conjecture: All terms of the Catalan-Mersenne sequence are prime.
theorem conjecture (n : ℕ) : (a n).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/7013.lean, line 58.
Sources
TheoremWolstenholme numbers#
Wolstenholme numbers: numerator of \(\sum_{k=1}^n \frac{1}{k^2}\).
References: - A007406
Quoted from FormalConjectures/OEIS/7406.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.
OeisA7406.conjecture
Open: stated without proof.
Conjecture: for \(n > 3\), \(\gcd(n, a(n-1)) = \text{A089026}(n)\). - Amiram Eldar and Thomas Ordowski, Jul 28 2019
theorem conjecture (n : ℕ) (hn : 3 < n) :
Nat.gcd n (a (n - 1)) = OeisA89026.a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/7406.lean, line 58.
Sources
TheoremSum of next \(n\) primes#
The sum of the primes in the \(n\)-th row of the prime number triangle:
\[a(n) = \sum_{i = 1 + n(n-1)/2}^{n + n(n-1)/2} p_i\]with \(a(0) = 0\).
References: - A007468
Quoted from FormalConjectures/OEIS/7468.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 4 test statements, counted here but not shown.
OeisA7468.conjecture
Open: stated without proof.
The only positive integer \(n\) such that \(a(n)\) is a perfect square is \(n=38\). - Carlos Eduardo Olivieri, Mar 09 2015
theorem conjecture (n : ℕ) (hn : 0 < n) : IsSquare (a n) ↔ n = 38
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/7468.lean, line 71.
Sources
TheoremLeast prime \(\ge n\)#
Least prime \(\ge n\) (version 1 of the "next prime" function).
References: - A007918
Quoted from FormalConjectures/OEIS/7918.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 4 test statements, counted here but not shown.
OeisA7918.conjecture1
Open: stated without proof.
According to the "k-tuple" conjecture, \(a(n)\) is the initial term of the lexicographically earliest increasing arithmetic progression of \(n\) primes; the corresponding common differences are given by A061558.
theorem conjecture1 (n : ℕ) (hn : 0 < n) :
a n = sInf { p0 : ℕ | ∃ d : ℕ, isApOfNPrimes n p0 d }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/7918.lean, line 82.
OeisA7918.conjecture2
Open: stated without proof.
If \(n > 1\), then \(a(n) < n^{n^{1/n}}\). - Thomas Ordowski, Feb 23 2023
theorem conjecture2 (n : ℕ) (hn : 1 < n) :
(a n : ℝ) < (n : ℝ) ^ ((n : ℝ) ^ (1 / (n : ℝ)))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/7918.lean, line 91.
Sources
TheoremPrime numbers at the beginning of the 20th century#
The sequence consists of \(1\) and the prime numbers. Today \(1\) is no longer regarded as a prime.
References: - A008578
Quoted from FormalConjectures/OEIS/8578.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.
OeisA8578.conjecture
Solved: stated here; a Lean proof is at https://github.com/otoi-lab/oeis-lean-proofs/blob/14f275b8b370bcf76213de10bb3f8fda84a6461e/OeisProofs/FC/A8578.lean#L18-L21.
"Conjecture: the sequence contains exactly those k such that sigma(k) > k*BigOmega(k)." - Irina Gerasimova, Jun 08 2013
Here \(\sigma(k)\) is the sum of the divisors of \(k\) and \(\Omega(k)\) is the number of prime factors of \(k\) counted with multiplicity. Both sides are false for \(k = 0\).
Solved by Claude (Anthropic) prompted by otoinobuo. The proof shows \(\sigma(k) < k P\) for the largest prime factor \(P\) of \(k\) and uses induction on \(k / P\).
theorem conjecture (k : ℕ) : A k ↔ k * cardFactors k < sigma 1 k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/8578.lean, line 66.
Sources
Theorem\(a(n)\) is the integer whose decimal digits are the first \(n+1\) decimal digits of \(\pi\)#
References: - A011545
Quoted from FormalConjectures/OEIS/11545.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 4 test statements, counted here but not shown.
OeisA11545.conjecture1
Open: stated without proof.
Wolfgang Haken (1977) conjectured that no term of this sequence is a perfect square, and estimated the probability that this conjecture is false to be smaller than \(10^-9\).
theorem conjecture1 : ∀ n, ¬ IsSquare (a n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/11545.lean, line 70.
OeisA11545.conjecture2
Open: stated without proof.
Number of collisions occurring in a system consisting of an infinitely massive, rigid wall at the origin, a ball with mass m stationary at position \(x_1 > 0\), and a ball with mass \((10^2n)m\) at position \(x_2 > x_1\) and rolling toward the origin, assuming perfectly elastic collisions and no friction.
Strictly speaking, this property, which is equivalent to the statement that the interval \((m\pi, \pi/\textrm{arctan}(1/m))\) does not contain an integer for all \(m = 10^n\), is not known to be true for sure. In other words, we do not know for certain that A332045 does not contain a power of \(10\).
theorem conjecture2 :
∀ n : ℕ, ¬ ∃ (k : ℤ),
(Real.pi * (10 : ℝ) ^ n.cast < k.cast) ∧
(k.cast < Real.pi / Real.arctan (1 / (10 : ℝ) ^ n.cast))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/11545.lean, line 85.
Sources
TheoremDenominator of sum of reciprocals of divisors#
Denominator of sum of reciprocals of divisors of \(n\):
\[\sum_{d \mid n} \frac{1}{d} = \frac{\sigma(n)}{n}\]in lowest terms.
References: - A017666
Quoted from FormalConjectures/OEIS/17666.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.
OeisA17666.conjecture
Open: stated without proof.
If \(a(n)\) is in A005153, then \(n\) is in A005153. - Jaycob Coleman, Sep 27 2014
We require \(0 < n\) because \(a(0) = 1\) is in A005153 (practical numbers), but \(0\) is not.
theorem conjecture (n : ℕ) (hn : 0 < n) : OeisA5153.A (a n) → OeisA5153.A n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/17666.lean, line 63.
Sources
TheoremA nonlinear recurrence sequence#
For even \(n\), \(a(n+2)\) is the greatest integer such that \(a(n+2)/a(n+1) < a(n+1)/a(n)\); for odd \(n\), the least integer such that \(a(n+2)/a(n+1) > a(n+1)/a(n)\); \(a(0) = 4, a(1) = 16\).
References: - A022030
Quoted from FormalConjectures/OEIS/22030.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 6 test statements, counted here but not shown.
OeisA22030.conjecture
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/oeis-a022030-lean/blob/f74afc2/lean/OeisA22030FC.lean#L270-L275.
Conjecture: \(a(n) = 4 a(n-1) - a(n-3) + a(n-4)\). - Colin Barker, Feb 16 2012
theorem conjecture (n : ℕ) (hn : 4 ≤ n) :
a n = 4 * a (n - 1) - a (n - 3) + a (n - 4)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/22030.lean, line 76.
Sources
TheoremDeterminant of Hankel matrix of the first \(2n-1\) prime numbers#
The determinant of the \(n \times n\) Hankel matrix whose entries are the first \(2n-1\) prime numbers. The matrix \(M\) has entries \(M_{i, j} = p_{i+j}\) for \(i, j \in \{0, \dots, n-1\}\), where \(p_k = \mathrm{Nat.nth\;Nat.Prime} (k)\) is the \(k\)-th prime starting at \(p_0=2\). \(a(0)=1\) by convention.
References: - A024356
Quoted from FormalConjectures/OEIS/24356.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 4 test statements, counted here but not shown.
OeisA24356.conjecture
Open: stated without proof.
"I conjecture that \(a(4)\) is the only zero. - Jon Perry, Mar 22 2004"
Stated as a biconditional: the claim that \(a(4)\) is the only zero asserts both that \(a(4) = 0\) and that no other index vanishes. A bare implication
a n = 0 → n = 4would be satisfied vacuously by a sequence with no zero at all. The existence direction is certified bya_4; the uniqueness direction is the open part.
theorem conjecture : ∀ n : ℕ, a n = 0 ↔ n = 4
Category research open; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/OEIS/24356.lean, line 85.
Sources
TheoremCombinatorial representation of the recurrence \(a(n+2) = 2a(n+1) + 2a(n)\)#
A028859 (OEIS): \(a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)\); \(a(0) = 1\), \(a(1) = 3\).
References: - A028859 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/28859.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.
OeisA28859.exists_finset_sequence
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/28859.wip.lean#L402.
Conjecture: The sequence a(n) is also the number of compositions of \(n\) into positive integers such that adjacent parts and the largest part differ by at most 1. - Gus Wiseman, May 19 2020
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem exists_finset_sequence (n : ℕ) :
let L := n + 1
let Sequence := Fin L → ℕ
let S : Set Sequence :=
{σ : Sequence |
L > 0 ∧
(∀ i : Fin L, σ i > 0) ∧
let max_val := Finset.sup Finset.univ σ
(∀ k : ℕ, 1 ≤ k ∧ k ≤ max_val → ∃ i : Fin L, σ i = k) ∧
(∀ i j : Fin L, i < j → j.val ≠ i.val + 1 → σ i ≥ σ j)}
∃ (F : Finset Sequence), (F : Set Sequence) = S ∧ F.card = a n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/28859.lean, line 74.
Sources
TheoremSmallest number \(k\) such that \(kn + 1\) is prime#
References: - A34693
Quoted from FormalConjectures/OEIS/34693.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: 4 open and 1 solved. It also has 5 test statements, counted here but not shown.
OeisA34693.exists_k
Open: stated without proof.
Conjecture: for every \(n > 1\) there exists a number \(k < n\) such that \(nk + 1\) is a prime.
theorem exists_k {n : ℕ} (hn : 1 < n) : ∃ k < n, (n * k + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34693.lean, line 61.
OeisA34693.exists_k_stronger
Open: stated without proof.
A stronger conjecture: for every n there exists a number \(k < 1 + n^{0.75}\) such that \(nk + 1\) is a prime.
theorem exists_k_stronger {n : ℕ} (hn : 0 < n) : ∃ k : ℕ,
k < 1 + (Real.nthRoot 4 n) ^ 3 ∧ (n * k + 1).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34693.lean, line 67.
OeisA34693.exists_k_best_possible
Proved here.
The expression \(1 + n^{0.74}\) does not work as an upper bound.
theorem exists_k_best_possible : ∃ n > (0 : ℕ), ∀ (k : ℕ),
k < 1 + (Real.nthRoot 100 n) ^ 74 → ¬(n * k + 1).Prime
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34693.lean, line 73.
OeisA34693.a_isBigO
Open: stated without proof.
Conjecture: \(a(n) = O(\log(n)\log(\log(n)))\).
theorem a_isBigO : (fun n ↦ (a n : ℝ)) =O[atTop] (fun n ↦ Real.log n * Real.log (Real.log n))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34693.lean, line 96.
OeisA34693.a_unbounded
Open: stated without proof.
Counter-conjecture to
a_isBigO: \(a(n) / (\log n \log \log n)\) is unbounded.
theorem a_unbounded : ¬BddAbove (Set.range fun n ↦ a n / (Real.log n * Real.log (Real.log n)))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34693.lean, line 101.
Sources
TheoremSmallest prime \(\equiv 1 \pmod n\)#
\[a(n) = \min \{p \in \mathbb{P} \mid p \equiv 1 \pmod n\}\]References: - A034694
Quoted from FormalConjectures/OEIS/34694.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.
OeisA34694.conjecture
Open: stated without proof.
"Conjecture: \(a(n) < n^2\) for \(n > 1\). - Thomas Ordowski, Dec 19 2016"
theorem conjecture (n : ℕ) (hn : 1 < n) : a n < n ^ 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/34694.lean, line 59.
Sources
TheoremHome primes (OEIS A037274)#
Starting from an integer \(n\geq 2\), list its prime factors in nondecreasing order with multiplicity, concatenate their decimal representations, and repeat. The home-prime conjecture says that this process always reaches a prime.
For example,
\[25 \longmapsto 55 \longmapsto 511 \longmapsto 773.\]References: * OEIS A037274 * M. Herman and J. Schiffman, Investigating home primes and their families, Mathematics Teacher 107 (2014), 606–614
Quoted from FormalConjectures/OEIS/37274.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.
OeisA37274.home_prime_conjecture
Open: stated without proof.
Every integer at least two reaches a home prime.
theorem home_prime_conjecture : ∀ n : ℕ, 2 ≤ n → ReachesPrime n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/37274.lean, line 59.
Sources
TheoremNumber of primes \(< n^3\)#
Number of primes strictly less than \(n^3\).
References: - A038098
Quoted from FormalConjectures/OEIS/38098.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.
OeisA38098.conjecture1
Open: stated without proof.
Conjecture (i): for any integer \(k > 2\), the sequence \(\pi(n^k)/n^k\) (\(n = 2, 3, \ldots\)) is strictly decreasing, where \(\pi(x)\) denotes the number of primes not exceeding \(x\). - Zhi-Wei Sun, Oct 17 2015
theorem conjecture1 (k : ℕ) (hk : 2 < k) (n : ℕ) (hn : 2 ≤ n) :
(Nat.primeCounting ((n + 1) ^ k) : ℚ) / ((n + 1) ^ k : ℚ) <
(Nat.primeCounting (n ^ k) : ℚ) / (n ^ k : ℚ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/38098.lean, line 67.
OeisA38098.conjecture2
Open: stated without proof.
Conjecture (ii): all the numbers \(\pi(n^2)/n^2\) (\(n = 1, 2, 3, \ldots\)) are pairwise distinct. Moreover, we have \(\pi(n^2)/n^2 > \pi((n+1)^2)/(n+1)^2\) for all \(n > 15646\). - Zhi-Wei Sun, Oct 17 2015
theorem conjecture2 :
(∀ m n : ℕ, 1 ≤ m → 1 ≤ n →
(Nat.primeCounting (m ^ 2) : ℚ) / (m ^ 2 : ℚ) =
(Nat.primeCounting (n ^ 2) : ℚ) / (n ^ 2 : ℚ) → m = n) ∧
(∀ n : ℕ, 15646 < n →
(Nat.primeCounting ((n + 1) ^ 2) : ℚ) / ((n + 1) ^ 2 : ℚ) <
(Nat.primeCounting (n ^ 2) : ℚ) / (n ^ 2 : ℚ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/38098.lean, line 78.
Sources
TheoremNumber of primes \(< n^2\)#
Number of primes strictly less than \(n^2\).
References: - A038107
Quoted from FormalConjectures/OEIS/38107.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.
OeisA38107.conjecture
Open: stated without proof.
Conjecture: all the numbers \(\sum_{i=j}^k \frac{1}{a(i)}\) with \(1 < j \le k\) have pairwise distinct fractional parts. - Zhi-Wei Sun, Sep 24 2015
theorem conjecture (j k j' k' : ℕ)
(hj : 1 < j) (hjk : j ≤ k) (hj' : 1 < j') (hj'k' : j' ≤ k')
(h_eq : Int.fract (∑ i ∈ Finset.Icc j k, (1 : ℝ) / (a i : ℝ)) =
Int.fract (∑ i ∈ Finset.Icc j' k', (1 : ℝ) / (a i : ℝ))) :
j = j' ∧ k = k'
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/38107.lean, line 71.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.