lean_workbook_plus_67012

Disproved

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

Verify the correctness of the expression $\binom{4}{4} + \binom{5}{4} + \binom{6}{4} + \binom{7}{4} + \binom{8}{4}$ and its evaluation to 112.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67012 (h₁ : 4 ≤ 4 ∧ 4 ≤ 5 ∧ 4 ≤ 6 ∧ 4 ≤ 7 ∧ 4 ≤ 8) : (Nat.choose 4 4 + Nat.choose 5 4 + Nat.choose 6 4 + Nat.choose 7 4 + Nat.choose 8 4) = 112   :=  by sorry

Source

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

View graph