Prove2Me

Binomial coefficient identity #41134

Proved
WorkbookCorrected.plus_41134

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

((115))−((53))=452(\binom{11}{5}) - (\binom{5}{3}) = 452

holds by direct arithmetic evaluation.

Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_41134, 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_41134 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_41134 : (Nat.choose 11 5) - (Nat.choose 5 3) = 452 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_41134; Apache-2.0; corrects Open node 037404d8-b847-4f1a-a4fd-f48399a549c1

View graph