Classic mathematics

Add 1 through n

A small recursive function and an induction proof of the triangular-number formula.

-- Top 100 #68: Add 1 through n
-- History: c. 1700 BCE · Babylonian arithmetic.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Writing twice the sum avoids division and makes the induction step a polynomial identity.
-- Scope: Proves 2(1+⋯+n)=n(n+1) for every natural n.
-- Source: https://lurch.plus/100/

def triangleSum : Nat → Nat
  | 0 => 0
  | n+1 => triangleSum n + (n+1)

theorem sum_formula (n : Nat) :
    2 * triangleSum n = n*(n+1) := by
  induction n with
  | zero => rfl
  | succ n ih => simp only [triangleSum]; grind

#eval triangleSum 100

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`grind`

Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

c. 1700 BCE · Babylonian arithmetic

Writing twice the sum avoids division and makes the induction step a polynomial identity.

Proves 2(1+⋯+n)=n(n+1) for every natural n.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

Exercise

Change the function to sum odd numbers. Can you prove the result is n²?