ErdosProblems · textbook · AMS 11
mediumknown result, no worker yet
Erdős Problem 1049
Theorem 1049 · Erdős
The classical Lambert series identity: $\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}\tau(n)n$.
Formal statement · Lean 4.lean
theorem lambert_series_eq_num_divisor_sum : ∀ t : ℚ,
∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1) =
∑' n : ℕ+, (n : ℕ).divisors.card / ((t : ℝ) ^ (n : ℕ)) := by
sorryProof. sorry
Nobody has tried yet.