lean_workbook_plus_44878

Open

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

Find the sum $\binom{22}{10}\binom{15}{0}+\binom{22}{9}\binom{15}{1}+\binom{22}{8}\binom{15}{2}+\cdots +\binom{22}{0}\binom{15}{10}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44878 (h₁ : 0 < 22) (h₂ : 0 < 15) : ∑ k in Finset.range 11, (Nat.choose 22 (10 - k) * Nat.choose 15 k) = 348330136   :=  by sorry

Source

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

View graph