Classic mathematics

A finite geometric series

Prove a familiar summation formula with recursion and induction.

-- Top 100 #66: A finite geometric series
-- History: c. 260 BCE · Archimedes tradition; date approximate.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Multiplying the sum by r shifts every term one place, leaving two endpoints after subtraction.
-- Scope: Proves (r−1)Σᵢ₌₀ⁿ⁻¹ rⁱ = rⁿ−1 for all integer r and natural n. It includes r=1 without division; no infinite limit is asserted.
-- Source: https://lurch.plus/100/

def geometricSum (r : Int) : Nat → Int
  | 0 => 0
  | n+1 => geometricSum r n + r^n

theorem geometric_formula (r : Int) (n : Nat) :
    (r-1)*geometricSum r n = r^n-1 := by
  induction n with
  | zero => simp only [geometricSum, Int.pow_zero]; grind
  | succ n ih => simp only [geometricSum, Int.pow_succ]; grind

#eval geometricSum 2 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.

`Int`

Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.

Background and proof scope

c. 260 BCE · Archimedes tradition; date approximate

Multiplying the sum by r shifts every term one place, leaving two endpoints after subtraction.

Proves (r−1)Σᵢ₌₀ⁿ⁻¹ rⁱ = rⁿ−1 for all integer r and natural n. It includes r=1 without division; no infinite limit is asserted.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

Exercise

Evaluate the sum at r=1 and r=−1. Why is avoiding division convenient?