Classic mathematics

The sum of squares

Repeat the induction pattern with a slightly richer polynomial.

-- Top 100 #77: The sum of squares
-- History: 1713 · Bernoulli’s power-sum milestone.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Multiplying by 6 clears the denominator of the familiar sum-of-squares formula.
-- Scope: Proves the square-sum formula for every n. This is one power-sum theorem, not the formula for arbitrary k.
-- Source: https://lurch.plus/100/

def squareSum : Nat → Nat
  | 0 => 0
  | n+1 => squareSum n + (n+1)^2

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

#eval squareSum 10

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

1713 · Bernoulli’s power-sum milestone

Multiplying by 6 clears the denominator of the familiar sum-of-squares formula.

Proves the square-sum formula for every n. This is one power-sum theorem, not the formula for arbitrary k.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

Exercise

Define a cube sum and conjecture a relationship with triangleSum squared.