lean_workbook_plus_39039

Proved

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

If $k$ is odd, then prove that $\binom{k+3}{2}\cdot (-1)^{k+1}+\binom{k+2}{2}\cdot (-1)^{k} = k+2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39039 (k : ℕ) (h : k % 2 = 1) : (k + 3).choose 2 * (-1 : ℤ) ^ (k + 1) + (k + 2).choose 2 * (-1) ^ k = (k + 2)   :=  by sorry

Source

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

View graph