Erdős Problem 1210: Er80 Correction
In [Er80] he claims he "did not state this quite correctly" in [Er77c]. The problem in [Er77c] which Erdős is presumably referring to states that if is the set of primes in then $\sum \frac{1}{q_i-n} < \sum_{p < m-n}\f...
Mathematical statement
In [Er80] he claims he "did not state this quite correctly" in [Er77c]. The problem in [Er77c] which Erdős is presumably referring to states that if is the set of primes in then .
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_1210.variants.er80_correction
theorem erdos_1210.variants.er80_correction : answer(sorry) ↔ ∃ C : ℝ, ∀ n m : ℕ, n < m → ∑ q ∈ (Ioc n m).filter Prime, (1 / ((q : ℝ) - n)) < (∑ p ∈ (range (m - n)).filter Prime, (1 / (p : ℝ))) + C := 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