Erdős problem 317
Is there some constant such that for every there exists some for with
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/317.lean∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)TextbookStatement only, no proof