ASI Prize

Back to Problems

sum_of_squares_of_prime_gaps_lower_bound

Specification

The prime number theorem immediately implies a lower bound of $\gg N(\log N)^2$ for the sum of squares of gaps between consecutive primes.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem sum_of_squares_of_prime_gaps_lower_bound :
    (fun (N : ℕ) => N * (log N)^2) =O[atTop]
    (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ))

ID: ErdosProblems__233__sum_of_squares_of_prime_gaps_lower_bound

Browse 300 unsolved math conjectures formalized in Lean 4

All Problems

Explore all 300 unsolved conjectures.

View problems →

ASI Prize documentation for formal verification pipeline

Verification Pipeline

How zero-trust verification works.

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.