Prove2Me

Binomial coefficient identity #48990

Disproved
WorkbookCorrected.plus_48990

by carlok · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

(choose(16+3)3−choose(11+3)3−choose(10+3)3−2∗choose(9+3)3+choose(5+3)3+2∗choose(4+3)3+2∗choose(3+3)3+choose(2+3)3)=55(choose (16 + 3) 3 - choose (11 + 3) 3 - choose (10 + 3) 3 - 2 * choose (9 + 3) 3 + choose (5 + 3) 3 + 2 * choose (4 + 3) 3 + 2 * choose (3 + 3) 3 + choose (2 + 3) 3) = 55

holds by direct arithmetic evaluation.

Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_48990, which omitted a compilable colon/type annotation and/or used a preamble of only Mathlib.Analysis.Complex.Basic.

Source: InternLM Lean-Workbook, record lean_workbook_plus_48990 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_48990 : ((Nat.choose (16 + 3) 3) - (Nat.choose (11 + 3) 3) - (Nat.choose (10 + 3) 3) - 2 * (Nat.choose (9 + 3) 3) + (Nat.choose (5 + 3) 3) + 2 * (Nat.choose (4 + 3) 3) + 2 * (Nat.choose (3 + 3) 3) + (Nat.choose (2 + 3) 3)) = 55 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_48990; Apache-2.0; corrects Open node c1b09ea6-7631-4bce-a57e-05fb3c48a4c9

View graph