Skip to main content

Proofs of ∑k<n. 2ᵏ = 2ⁿ-1

Prove that \[ 1 + 2 + 2^2 + 2^3 + ... + 2^{n-1} = 2^n - 1 \]

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

open Finset Nat

variable (n : ℕ)

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
by sorry

1. Proof in natural language

By induction on \(n\).

Base case: Let \(n = 0\). Then, \begin{align} \sum_{k<0} 2^k &= 0 \newline &= 2^0 - 1 \newline &= 2^n - 1 \newline \end{align}

Induction step: Let \(n = m+1\) and suppose the induction hypothesis (IH) \[ \sum_{k<m} 2^k = 2^m-1 \] Then, \begin{align} \sum_{k<n} 2^k &= \sum_{k<m+1} 2^k \newline &= \sum_{k<m} 2^k + 2^m \newline &= (2^m - 1) + 2^m &&\text{[por HI]} \newline &= (2^m + 2^m) - 1 \newline &= 2^{m + 1} - 1 \newline &= 2^n - 1 \end{align}

2. Proofs with Lean4

import Mathlib.Tactic

open Finset Nat

variable (n : ℕ)

-- Proof 1
-- =======

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
by
  induction n with
  | zero =>
    -- ⊢ ∑ k ∈ range 0, 2 ^ k = 2 ^ 0 - 1
    calc ∑ k ∈ range 0, 2 ^ k
         = 0                   := sum_range_zero (2 ^ .)
       _ = 2 ^ 0 - 1           := by omega
  | succ m HI =>
    -- m : ℕ
    -- HI : ∑ k ∈ range m, 2 ^ k = 2 ^ m - 1
    -- ⊢ ∑ k ∈ range (m + 1), 2 ^ k = 2 ^ (m + 1) - 1
    have h1 : (2^m - 1) + 2^m = (2^m + 2^m) - 1 := by
      have h2 : 2^m ≥ 1 := Nat.one_le_two_pow
      omega
    calc ∑ k in range (m + 1), 2^k
       = ∑ k in range m, (2^k) + 2^m
           := sum_range_succ (2 ^ .) m
     _ = (2^m - 1) + 2^m
           := congrArg (. + 2^m) HI
     _ = (2^m + 2^m) - 1
           := h1
     _ = 2^(m + 1) - 1
           := congrArg (. - 1) (two_pow_succ m).symm

-- Proof 2
-- =======

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
by
  induction n with
  | zero =>
    -- ⊢ ∑ k ∈ range 0, 2 ^ k = 2 ^ 0 - 1
    simp
  | succ m HI =>
    -- m : ℕ
    -- HI : ∑ k ∈ range m, 2 ^ k = 2 ^ m - 1
    -- ⊢ ∑ k ∈ range (m + 1), 2 ^ k = 2 ^ (m + 1) - 1
    have h1 : (2^m - 1) + 2^m = (2^m + 2^m) - 1 := by
      have h2 : 2^m ≥ 1 := Nat.one_le_two_pow
      omega
    calc ∑ k in range (m + 1), 2^k
       = ∑ k in range m, (2^k) + 2^m := sum_range_succ (2 ^ .) m
     _ = (2^m - 1) + 2^m             := by linarith
     _ = (2^m + 2^m) - 1             := h1
     _ = 2^(m + 1) - 1               := by omega

-- Used lemmas
-- ===========

-- variable (f : ℕ → ℕ)
-- #check (Nat.one_le_two_pow : 1 ≤ 2 ^ n)
-- #check (Nat.two_pow_succ n : 2 ^ (n + 1) = 2 ^ n + 2 ^ n)
-- #check (sum_range_succ f n : ∑ x ∈ range (n+1), f x = ∑ x ∈ range n, f x + f n)
-- #check (sum_range_zero f : ∑ k ∈ range 0, f k = 0)

You can interact with the previous proofs at Lean 4 Web.

3. Proofs with Isabelle/HOL

theory Sum_of_powers_of_two
imports Main
begin

(* Proof 1 *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (∑k≤n. (2::nat)^k) + 2^Suc n"
    by simp
  also have "… = (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  also have "… = 2^(Suc n + 1) - 1"
    by simp
  finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" .
qed

(* Proof 2 *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1"
    by simp
qed

(* Proof 3 *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

(* Proof 4 *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
by (induct n) simp_all

end

Note: The code for the previous proofs can be found in the Calculemus repository on GitHub.