lean_workbook_plus_60317
OpenThe common approach is to use telescoping sums. Let's look at the general term: the th term is . We know that for telescoping sums to help, we need to express the general terms as a difference, so the terms can cancel out. We know that for some real and . Solving, we see that and . Now we can use telescoping sums to find our answer. We have . We see a lot of terms canceling out, leaving us with as our answer .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60317 : ∑ k in (Finset.range 50), (1 : ℝ) / (k * (k + 1)) = 49 / 50 := by sorry
Source