Prove2Me

lean_workbook_plus_77340

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

∑i=1100(5i−5i−1) \sum_{i=1}^{100} (5^i - 5^{i-1})

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77340 : ∑ i in Finset.Icc 1 100, (5^i - 5^(i-1)) = 5^100 - 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph