lean_workbook_plus_49771

Open

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

Prove that $\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}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49771 : ∑ m in Finset.range 16, ∑ n in Finset.range (16 - m), (Nat.choose (m + n) m * Nat.choose 15 (m + n) * 5 ^ n) = ∑ m in Finset.range 16, (Nat.choose 15 m * 6 ^ (15 - m))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph