Prove2Me

Elementary arithmetic identity #21622

Proved
WorkbookCorrected.plus_21622

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

10=5+5∧11=5+6∧12=6+6∧13=5+6+2∧14=5+5+2+210 = 5 + 5 ∧ 11 = 5 + 6 ∧ 12 = 6 + 6 ∧ 13 = 5 + 6 + 2 ∧ 14 = 5 + 5 + 2 + 2

holds by direct arithmetic evaluation.

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

Preamble
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_21622 : (10 = 5 + 5) ∧ (11 = 5 + 6) ∧ (12 = 6 + 6) ∧ (13 = 5 + 6 + 2) ∧ (14 = 5 + 5 + 2 + 2) := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_21622; Apache-2.0; corrects Open node 8ba47cb9-52d9-4506-a630-7c20c13b45f7

View graph