Prove2Me

lean_workbook_plus_64416

Open

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

Explain the combinatorial interpretation of the polynomial p(x)=(x0)+(x1)+…+(x1007)p(x) = {x \choose 0} + {x \choose 1} + \ldots + {x \choose 1007} and how it relates to finding p(2015)p(2015).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64416 (p : ℕ → ℕ) (hp : ∀ x, p x = ∑ i in Finset.range 1008, Nat.choose x i) : p 2015 = 2^2014   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph