ErdosProblems · textbook · AMS 11
mediumknown result, no worker yet
Erdős Problem 317
Theorem 317 · Erdős
Inequality in erdos_317.variants.claim2 is obvious, the problem is strict inequality.
Formal statement · Lean 4.lean
lemma claim2_inequality : ∀ᶠ 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
sorryProof. sorry
Nobody has tried yet.