Nicomachus’s theorem
Prove the Nicomachus's theorem which states that the sum of the cubes of the first \(n\) natural numbers is equal to the square of the sum of the first \(n\) natural numbers; that is, for any natural number n we have \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Nat.Defs import Mathlib.Tactic open Nat variable ( n : ℕ) def sum : ℕ → ℕ | 0 => 0 | succ n => sum n + (n+1) def sumCubes : ℕ → ℕ | 0 => 0 | n+1 => sumCubes n + (n+1)^3 example : sumCubes n = (sum n)^2 := by sorry
1. Proof in natural language
It is a consequence of the formulas for the sum of the first \(n\) natural numbers and the sum of the cubes of the first \(n\) natural numbers; that is,
- Lemma 1: \[1 + 2 + ... + n = \dfrac{n(n+1)}{2} \]
- Lemma 2: \[1^3 + 2^3 + ... + n^3 = \dfrac{(n(n+1))^2}{4} \]
In fact,
\begin{align} 1^3 + 2^3 + ... + n^3 &= \dfrac{(n(n+1))^2}{4} &&\text{[by Lemma 2]} \newline &= \dfrac{2(1 + 2 + ... + n)^2}{4} &&\text{[by Lemma 1]} \newline &= (1 + 2 + ... + n)^2 \end{align}
Lemma 1 is equivalent to \[ 2(1 + 2 + ... + n) = n(n+1) \] which is proved by induction:
Base case: For \(n = 0\), the sum is \(0\) and \[ 2·0 = 0(0+1) \]
Inductive step: Assume the inductive hypothesis: \[ 2(1 + 2 + ... + n) = n(n+1) \tag{IH} \] Then, \begin{align} 2(1 + 2 + ... + n + (n+1)) &= 2(1 + 2 + ... + n) + 2(n+1) \newline &= n(n+1) + 2(n+1) &&\text{[by IH]} \newline &= (n+2)(n+1) \newline &= (n+1)((n+1)+1) \end{align}
Lemma 2 is equivalent to \[ 4(1^3 + 2^3 + ... + n^3) = (n(n+1))^2 \] which is proved by induction:
Base case: For \(n = 0\), the sum is \(0\) and \[ 4·0 = (0(0+1))^2 \] Inductive step: Assume the inductive hypothesis: \[ 4(1^3 + 2^3 + ... + n^3) = (n(n+1))^2 \tag{IH} \] Then, \begin{align} 4(1^3 + 2^3 + ... + n^3 + (n+1)^3) &= 4(1^3 + 2^3 + ... + n^3) + 4(n+1)^3 \newline &= (n(n+1))^2 + 4(n+1)^3 \newline &= (n+1)^2(n^2 + 4n + 4) \newline &= ((n+1)((n+1)+1))^2 \end{align}
2. Proofs with Lean4
import Mathlib.Data.Nat.Defs import Mathlib.Tactic open Nat variable (m n : ℕ) set_option pp.fieldNotation false -- (sum n) is the sum of the first n natural numbers. def sum : ℕ → ℕ | 0 => 0 | succ n => sum n + (n+1) @[simp] lemma suma_zero : sum 0 = 0 := rfl @[simp] lemma suma_succ : sum (n + 1) = sum n + (n+1) := rfl -- (sumCubes n) is the sum of the cubes of the first n natural numbers. @[simp] def sumCubes : ℕ → ℕ | 0 => 0 | n+1 => sumCubes n + (n+1)^3 -- Lemma 1: 2(1 + 2 + ... + n) = n(n+1) -- Proof 1 of Lemma 1 -- ================== example : 2 * sum n = n * (n + 1) := by induction n with | zero => -- ⊢ 2 * sum 0 = 0 * (0 + 1) calc 2 * sum 0 = 2 * 0 := congrArg (2 * .) suma_zero _ = 0 := mul_zero 2 _ = 0 * (0 + 1) := zero_mul (0 + 1) | succ n HI => -- n : ℕ -- HI : 2 * sum n = n * (n + 1) -- ⊢ 2 * sum (n + 1) = (n + 1) * (n + 1 + 1) calc 2 * sum (n + 1) = 2 * (sum n + (n + 1)) := congrArg (2 * .) (suma_succ n) _ = 2 * sum n + 2 * (n + 1) := mul_add 2 (sum n) (n + 1) _ = n * (n + 1) + 2 * (n + 1) := congrArg (. + 2 * (n + 1)) HI _ = (n + 2) * (n + 1) := (add_mul n 2 (n + 1)).symm _ = (n + 1) * (n + 2) := mul_comm (n + 2) (n + 1) -- Proof 2 of Lemma 1 -- ================== example : 2 * sum n = n * (n + 1) := by induction n with | zero => -- ⊢ 2 * sum 0 = 0 * (0 + 1) calc 2 * sum 0 = 2 * 0 := rfl _ = 0 := rfl _ = 0 * (0 + 1) := rfl | succ n HI => -- n : ℕ -- HI : 2 * sum n = n * (n + 1) -- ⊢ 2 * sum (n + 1) = (n + 1) * (n + 1 + 1) calc 2 * sum (n + 1) = 2 * (sum n + (n + 1)) := rfl _ = 2 * sum n + 2 * (n + 1) := by ring _ = n * (n + 1) + 2 * (n + 1) := by simp [HI] _ = (n + 2) * (n + 1) := by ring _ = (n + 1) * (n + 2) := by ring -- Proof 3 of Lemma 1 -- ================== example : 2 * sum n = n * (n + 1) := by induction n with | zero => -- ⊢ 2 * sum 0 = 0 * (0 + 1) rfl | succ n HI => -- n : ℕ -- HI : 2 * sum n = n * (n + 1) -- ⊢ 2 * sum (n + 1) = (n + 1) * (n + 1 + 1) calc 2 * sum (n + 1) = 2 * (sum n + (n + 1)) := rfl _ = 2 * sum n + 2 * (n + 1) := by ring _ = n * (n + 1) + 2 * (n + 1) := by simp [HI] _ = (n + 1) * (n + 2) := by ring -- Proof 4 of Lemma 1 -- ================== lemma sum_formula : 2 * sum n = n * (n + 1) := by induction n with | zero => rfl | succ n HI => unfold sum ; linarith [HI] -- Lemma 2: 4(1³ + 2³ + ... + n³) = (n(n+1))² -- Proof 1 of Lemma 2 -- ================== example : 4 * sumCubes n = (n*(n+1))^2 := by induction n with | zero => -- ⊢ 4 * sumCubes 0 = (0 * (0 + 1)) ^ 2 calc 4 * sumCubes 0 = 4 * 0 := by simp only [sumCubes] _ = (0 * (0 + 1)) ^ 2 := by simp | succ m HI => -- m : ℕ -- HI : 4 * sumCubes m = (m * (m + 1)) ^ 2 -- ⊢ 4 * sumCubes (m + 1) = ((m + 1) * (m + 1 + 1)) ^ 2 calc 4 * sumCubes (m + 1) = 4 * (sumCubes m + (m+1)^3) := by simp only [sumCubes] _ = 4 * sumCubes m + 4*(m+1)^3 := by ring _ = (m*(m+1))^2 + 4*(m+1)^3 := congrArg (. + 4*(m+1)^3) HI _ = (m+1)^2*(m^2+4*m+4) := by ring _ = (m+1)^2*(m+2)^2 := by ring _ = ((m+1)*(m+2))^2 := by ring _ = ((m+1) * (m+1+1))^2 := by simp -- Proof 2 of Lemma 2 -- ================== lemma sumCubes_formula : 4 * sumCubes n = (n*(n+1))^2 := by induction n with | zero => simp | succ m HI => calc 4 * sumCubes (m+1) = 4 * sumCubes m + 4*(m+1)^3 := by {simp ; ring_nf} _ = (m*(m+1))^2 + 4*(m+1)^3 := congrArg (. + 4*(m+1)^3) HI _ = ((m+1)*(m+2))^2 := by ring _ = ((m+1) * (m+1+1)) ^ 2 := by simp -- Nicomachus's theorem example : sumCubes n = (sum n)^2 := by have h1 : 4 * sumCubes n = 4 * (sum n)^2 := calc 4 * sumCubes n = (n*(n+1))^2 := by simp only [sumCubes_formula] _ = (2 * sum n)^2 := by simp only [sum_formula] _ = 4 * (sum n)^2 := by ring linarith -- Used lemmas -- =========== -- variable (a b c : ℕ) -- #check (add_mul a b c : (a + b) * c = a * c + b * c) -- #check (mul_add a b c : a * (b + c) = a * b + a * c) -- #check (mul_comm a b : a * b = b * a) -- #check (mul_zero a : a * 0 = 0) -- #check (zero_mul a : 0 * a = 0)
You can interact with the previous proofs at Lean 4 Web.
3. Demostraciones con Isabelle/HOL
theory Nicomachus_theorem imports Main begin (* (sum n) is the sum of the first n natural numbers. *) fun sum :: "nat ⇒ nat" where "sum 0 = 0" | "sum (Suc n) = sum n + Suc n" (* (sumCubes n) is the sum of the cubes of the first n natural numbers. *) fun sumCubes :: "nat ⇒ nat" where "sumCubes 0 = 0" | "sumCubes (Suc n) = sumCubes n + (Suc n)^3" (* Lemma 1: 2(1 + 2 + ... + n) = n(n+1) *) (* Proof 1 of Lemma 1 *) lemma "2 * sum n = n^2 + n" proof (induct n) show "2 * sum 0 = 0^2 + 0" by simp next fix n assume "2 * sum n = n^2 + n" then have "2 * sum (Suc n) = n^2 + n + 2 + 2 * n" by simp also have "… = (Suc n)^2 + Suc n" by (simp add: power2_eq_square) finally show "2 * sum (Suc n) = (Suc n)^2 + Suc n" by this qed (* Proof 2 of Lemma 1 *) lemma sum_formula: "2 * sum n = n^2 + n" by (induct n) (auto simp add: power2_eq_square) (* Lemma 2: 4(1³ + 2³ + ... + n³) = (n(n+1))² *) (* Proof 1 of Lemma 2 *) lemma "4 * sumCubes n = (n^2 + n)^2" proof (induct n) show "4 * sumCubes 0 = (0^2 + 0)^2" by simp next fix n assume "4 * sumCubes n = (n^2 + n)^2" then have "4 * sumCubes (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3" by simp then show "4 * sumCubes (Suc n) = ((Suc n)^2 + Suc n)^2" by (simp add: algebra_simps power2_eq_square power3_eq_cube ) qed (* Proof 2 of Lemma 2 *) lemma sumCubes_formula: "4 * sumCubes n = (n^2 + n)^2" by (induct n) (auto simp add: algebra_simps power2_eq_square power3_eq_cube) (* Auxiliary lemma *) lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2" by (simp add: power2_eq_square) (* Nicomachus’s theorem. *) theorem Nicomachus : "sumCubes n = (sum n)^2" by (simp only: sum_formula sumCubes_formula aux) end