Prove PrimeGaps (openai/math family 026: Positive lower density of large prime gaps) in Lean 4 with Mathlib…
Prove PrimeGaps (openai/math family 026: Positive lower density of large prime gaps) in Lean 4 with Mathlib…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 026 of the release, Positive lower density of large prime gaps (Number theory). The…
The task
Context: this statement belongs to family 026 of the release, *Positive lower density of large prime gaps* (Number theory). The family as a whole: For every fixed $C>0$, a positive proportion of consecutive prime gaps exceed $C\log p_n$, throughout every sufficiently large initial segment of the primes. The…
Part of raising-heart/openai-math.