Prove2Me

Lean-Workbook Syntax 49771: A finite binomial convolution identity

Proved
WorkbookSyntax.plus_49771

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

lean-workbookrepaired-notationsource-checked

∑m=015∑n=015−m(m+nm)(15m+n)5n=∑m=015(15m)615−m\sum_{m=0}^{15}\sum_{n=0}^{15-m}\binom{m+n}{m}\binom{15}{m+n}5^n=\sum_{m=0}^{15}\binom{15}{m}6^{15-m}.

Source: Lean-Workbook row lean_workbook_plus_49771 (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_49771 : ∑ m ∈ Finset.range 16, ∑ n ∈ Finset.range (16 - m), (Nat.choose (m + n) m * Nat.choose 15 (m + n) * 5 ^ n) = ∑ m ∈ Finset.range 16, (Nat.choose 15 m * 6 ^ (15 - m))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_49771; immutable original Prove2Me node 7c709cbb-5fcf-49fe-b6f6-8a68e9b4b68c

View graph