ErdosProblems · textbook · AMS 11

mediumknown result, no worker yet

Erdős Problem 68

Theorem 68 · Erdős

∑n=2∞1n!−1=∑n=2∞∑k=1∞1(n!)k\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}

Formal statement · Lean 4.lean
theorem sum_factorial_inv_eq_geometric :
    let f (n k : ℕ) : ℝ := 1 / ((n + 2).factorial : ℝ) ^ (k + 1)
    ∑' n : ℕ, (1 : ℝ) / ((n + 2).factorial - 1) = ∑' n : ℕ, ∑' k : ℕ, f n k := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗