Prove2Me

Lean-Workbook Syntax 64416: Half of an odd binomial row

Proved
WorkbookSyntax.plus_64416

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

lean-workbookrepaired-notationsource-checked

If p(x)=∑i=01007(xi)p(x)=\sum_{i=0}^{1007}\binom{x}{i} for natural xx, then p(2015)=22014p(2015)=2^{2014}.

Source: Lean-Workbook row lean_workbook_plus_64416 (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_64416 (p : ℕ → ℕ) (hp : ∀ x, p x = ∑ i ∈ Finset.range 1008, Nat.choose x i) : p 2015 = 2^2014   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_64416; immutable original Prove2Me node 21698a2b-044e-44d3-87a1-6c62746dd3f3

View graph