Prove2Me

Pascal’s recurrence for pairs and triples

Proved
WorkbookRestored.plus_10203

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

lean-workbookrestored-importssource-checked

For every natural number rr,

(r+12)+(r+13)=(r+23).\binom{r+1}2+\binom{r+1}3=\binom{r+2}3.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_10203 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Choose.Basic
open Nat
Formal statement
theorem WorkbookRestored.plus_10203 (r : ℕ) : choose (r + 1) 2 + choose (r + 1) 3 = choose (r + 2) 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_10203; original Prove2Me node 94ba9c8f-ec8f-4fc5-8365-2adc7a7f0d44; Apache-2.0

View graph