Prove2Me

Lean-Workbook Syntax 68935: A sum of consecutive integer products

Proved
WorkbookSyntax.plus_68935

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

∑k=199k(k+1)=333300\sum_{k=1}^{99}k(k+1)=333300.

Source: Lean-Workbook row lean_workbook_plus_68935 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble
import Mathlib.Algebra.BigOperators.Intervals
Formal statement
theorem WorkbookSyntax.plus_68935 :
  ∑ k ∈ (Finset.Icc 1 99), (k * (k + 1)) = 333300   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_68935; immutable original Prove2Me node 20c3542c-3d3f-4905-827d-b3954fe9f616

View graph