Prove2Me

lean_workbook_plus_68935

Open

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

Indeed. Solution using sigma/sum notation\nWe have 1⋅2+2⋅3+…+99⋅100=1 \cdot 2 + 2 \cdot 3 + \ldots + 99 \cdot 100 =\n$$ \sum_{k = 1}^{99} k \cdot (k + 1) = \sum_{k = 1}^{99} k^2 + k = $\n

∑k=199k2+∑k=199k\sum_{k = 1}^{99} k^2 + \sum_{k = 1}^{99} k

By the sums of integers and squares formulae, we have\n

∑k=199k2=99⋅100⋅1996\sum_{k = 1}^{99} k^2 = \frac{99 \cdot 100 \cdot 199}{6}

\n

∑k=199k=99⋅1002=99⋅100⋅36\sum_{k = 1}^{99} k = \frac{99 \cdot 100}{2} = \frac{99 \cdot 100 \cdot 3}{6}

Therefore, the desired sum is 99⋅100⋅2026=33⋅100⋅101=333300\frac{99 \cdot 100 \cdot 202}{6} = 33 \cdot 100 \cdot 101 = \boxed{333300}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68935 :
  ∑ k in (Finset.Icc 1 99), (k * (k + 1)) = 333300   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph