Erdős Problem 238
Let c₁, c₂ > 0. Is it true that for any sufficiently large x, there exists more than c₁ * log x many consecutive primes ≤ x such that the difference between any two is > c₂?
Mathematical statement
Let c₁, c₂ > 0. Is it true that for any sufficiently large x, there exists more than
c₁ * log x many consecutive primes ≤ x such that the difference between any two is > c₂?
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_238
theorem erdos_238 : answer(sorry) ↔ ∀ᵉ (c₁ > 0) (c₂ > 0), ∀ᶠ (x : ℝ) in atTop, ∃ (k : ℕ), c₁ * log x < k ∧ ∃ f : Fin k → ℕ, ∃ m, (∀ i, f i ≤ x ∧ f i = (m + i.1).nth Nat.Prime) ∧ ∀ i : Fin (k - 1), c₂ < primeGap (m + i.1) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References