Ben Green's Open Problem 46: Improve Upper Conjectured
It seems very likely that we must have [Gr24].
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.1194 of 1194 statement records
17 source collections · 43 mathematical fields
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 .
Conjecture: the sequence A228828 is infinite.
The conjecture for sequence A231201: for any , there exist such that and is prime.
*Zhi-Wei Sun's Conjecture (A232174)**: Any integer can be written as with such that both and are prime.
*Zhi-Wei Sun's Conjecture (A239957)**: Every prime has a primitive root of the form , where is an integer.
*Zhi-Wei Sun's 1680-Conjecture (A280831)**: Any nonnegative integer can be written as with nonnegative integers such that is a square.
*Zhi-Wei Sun's Conjecture (A281976)**: Any integer can be written as with nonnegative integers and , such that both and are squares.
*Zhi-Wei Sun's Conjecture (A287616)**: Any nonnegative integer can be written as the sum of a triangular number , a generalized pentagonal number , and a generalized heptagonal number , where are nonnegative integers.