Back to Problems
erdos_233.variant
Specification
Cramér proved an upper bound of $O(N(\log N)^4)$ conditional on the Riemann hypothesis.
Lean 4 Statement
theorem erdos_233.variant (h : RiemannHypothesis) :
(fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^4
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.