Erdős problem 317
Is there some constant such that for every there exists some for with
Sources
FormalConjectures/ErdosProblems/
317.lean
Retained formal statement
erdos_317.variants.claim2 fails for small , for example
¬∀ (δ : 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