Elementary arithmetic identity #82619

Disproved

WorkbookCorrected.plus_82619

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

2 + 12 + 30 + 56 + 90 + 132 + 182 + 240 + 306 + 380 + 462 + 552 + 650 + 756 + 870 + 992 + 1122 + 1260 + 1406 + 1560 + 1722 + 1892 + 2070 + 2256 + 2450 + 2652 + 2862 + 3080 + 3306 + 3540 + 3782 + 4032 + 4290 + 4556 + 4830 + 5112 + 5402 + 5700 + 6006 + 6320 + 6642 + 6972 + 7310 + 7656 + 8010 + 8372 + 8742 + 9120 + 9506 + 9900 = 24500

holds by direct arithmetic evaluation.

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

Preamble

import Mathlib.Tactic.NormNum

Formal statement

theorem WorkbookCorrected.plus_82619 : 2 + 12 + 30 + 56 + 90 + 132 + 182 + 240 + 306 + 380 + 462 + 552 + 650 + 756 + 870 + 992 + 1122 + 1260 + 1406 + 1560 + 1722 + 1892 + 2070 + 2256 + 2450 + 2652 + 2862 + 3080 + 3306 + 3540 + 3782 + 4032 + 4290 + 4556 + 4830 + 5112 + 5402 + 5700 + 6006 + 6320 + 6642 + 6972 + 7310 + 7656 + 8010 + 8372 + 8742 + 9120 + 9506 + 9900 = 24500 := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_82619; Apache-2.0; corrects Open node 621c9aeb-6d14-4f80-80a2-f1b7ba5b04f4

View graph