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.