therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 317: Claim2

Is it true that for sufficiently large nn, for any δk∈{−1,0,1}\delta_k\in \{-1,0,1\}, ∣∑1≤k≤nδkk∣>1[1,…,n]\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]} whenever the left-hand side is not zero?

Number theoryAMS 11

Mathematical statement

Is it true that for sufficiently large nn, for any δk∈{−1,0,1}\delta_k\in \{-1,0,1\}, ∣∑1≤k≤nδkk∣>1[1,…,n]\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]} whenever the left-hand side is not zero?

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_317.variants.claim2

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_317.variants.claim2 : answer(sorry) ↔    ∀ᶠ n in atTop, ∀ δ : (Fin n) → ℚ, δ '' Set.univ ⊆ {-1,0,1} →    letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))|    lhs ≠ 0 → lhs > 1 / (Icc 1 n).lcm id := 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

Pinned Formal Conjectures sourceformalizationerdosproblems.com/317background