Erdős problem 317 · problems.science

Is there some constant $c>0$ such that for every $n\geq 1$ there exists some $\delta_k\in \{-1,0,1\}$ for $1\leq k\leq n$ with $0< \left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert < \frac{c}{2^n}?$

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

317.lean

Retained formal statement3 of 4

Is it true that for sufficiently large $n$ , for any $\delta_k\in \{-1,0,1\}$ , $\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?

FormalConjectures/ErdosProblems/317.leanErdos317.erdos_317.variants.claim24 linesExact file

1sorry ↔2  ∀ᶠ (n : ℕ) in Filter.atTop,3    ∀ (δ : Fin n → ℚ),4      δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 n).lcm id)

OpenStatement only, no proof

Sources

Search problems.science