Nicomachuss_Theorem
Provednumber-theoryproofwiki
The sum of the first n cubes equals the square of the sum of the first n natural numbers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Nicomachuss_Theorem (n : ℕ) : (∑ i : Fin n, ((i : ℕ) + 1)) ^ 2 = ∑ i : Fin n, ((i : ℕ) + 1) ^ 3 := by sorry
Source