lean_workbook_plus_34532

Open

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

Derive the formula $1 + 2 + 3 + \cdots + (n - 1) + n = \frac{n(n + 1)}{2}$ for the sum of the first n natural numbers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34532 (n : ℕ) : (∑ i in Finset.range (n + 1), i) = n * (n + 1) / 2   :=  by sorry

Source