Erdős Problem 979
Let , and let count the number of solutions to , where the are prime numbers. Is it true that ?
Questions, not proof records
Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.
sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.Let , and let count the number of solutions to , where the are prime numbers. Is it true that ?
Is it true that, for every prime , there is a prime which is a primitive root modulo ?
Let be a set of integers. Is there a set of size such that the restricted sumset is disjoint from ?
Suppose that is open and has measure greater than . Is there a solution to with ?
Sieve by removing half the residue classes mod , for primes . Does the remaining set have size at most ?
We interpret "half the residue classes" as .
We conjecture that the best-known lower bound can be improved.
We conjecture that the best-known upper bound can be improved.
It seems very likely that we must have [Gr24].
Suppose that a large sieve process leaves a set of quadratic size. Is that set quadratic?
The following very particular instance is probably the simplest [Gr24]: Suppose that is a set with the property that for all sufficiently large . Is it true that either , or is contained in the image of under a quadratic map ?
Is there an absolute constant such that, whenever is a set of squares with , the sumset satisfies ?
Suppose that contains the first squares. Is ?
It is known that necessarily , whilst in the other direction there do exist such with for any .
Let be a large prime, and let be the set of all primes less than . Is every congruent to some product where ?
Is there always a sum of two squares between and ? We formalize this as an eventual statement for sufficiently large real .
Does Ulam's sequence have positive density?
If and are integers, then must be an integer.
Is 2n the complexity of 2^n for 0 < n?
The Riemann Hypothesis: all non-trivial zeros of the Riemann zeta function have real part . That is, if , , and is not a trivial zero for some , then .
This is the official Millennium Prize Problem as posed by the Clay Mathematics Institute.
This uses the RiemannHypothesis type from Mathlib, which is defined as
∀ (s : ℂ), riemannZeta s = 0 → (¬∃ n : ℕ, s = -2 * (n + 1)) → s ≠ 1 → s.re = 1 / 2.
The Generalized Riemann Hypothesis asserts that all the non-trivial zeros of the Dirichlet -function of a primitive Dirichlet character have real part .