Prove2Me

Elementary arithmetic identity #13311

Proved
WorkbookCorrected.plus_13311

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

0+1+2+3+4+5+6+7+8+9+10+11+12=780 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 = 78

holds by direct arithmetic evaluation.

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

Preamble
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_13311 : 0 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 = 78 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_13311; Apache-2.0; corrects Open node 0cc382b2-5442-4618-94f0-4a0b8398c599

View graph