Lean-Workbook Syntax 58729: An alternating even-index binomial sum

Proved

WorkbookSyntax.plus_58729

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

lean-workbookrepaired-notationsource-checked

$\sum_{k=0}^{49}(-1)^k\binom{99}{2k}=-2^{49}$ .

Source: Lean-Workbook row lean_workbook_plus_58729 (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.Data.Nat.Choose.Sum

Formal statement

theorem WorkbookSyntax.plus_58729 (n : ℕ) : ∑ k ∈ Finset.range (49+1), (-1 : ℤ)^k * (99).choose (2 * k) = (-1 : ℤ)^49 * 2^49   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_58729; immutable original Prove2Me node 2bdc2b86-e76c-46f9-a2f6-05046072a602

View graph