Skip to content

Erdős problem 317

Is there some constant c>0c>0 such that for every n1n\geq 1 there exists some δk{1,0,1}\delta_k\in \{-1,0,1\} for 1kn1\leq k\leq n with 0<1knδkk<c2n?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 statement4 of 4

erdos_317.variants.claim2 fails for small nn, for example 121314=112.\frac{1}{2}-\frac{1}{3}-\frac{1}{4}=-\frac{1}{12}.

FormalConjectures/ErdosProblems/317.leanErdos317.erdos_317.variants.counterexample2 linesExact file
¬∀ (δ : Fin 4 → ℚ),    δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 4).lcm id)
TextbookStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page