--- /dev/null
+++ b/Mathlib/Unsorry/NicomachusSumCubes.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Chris Barlow. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Barlow
+-/
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.Linarith
+
+theorem nicomachus_sum_cubes (n : ℕ) :
+    (∑ k ∈ Finset.range n, k ^ 3) = (∑ k ∈ Finset.range n, k) ^ 2 := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [Finset.sum_range_succ, Finset.sum_range_succ, ih]
+    cases n with
+    | zero => simp
+    | succ m =>
+      set S := ∑ k ∈ Finset.range (m + 1), k
+      have h : S * 2 = (m + 1) * m := by
+        have h' := Finset.sum_range_id_mul_two (m + 1)
+        rw [show (m + 1) - 1 = m from by omega] at h'
+        exact h'
+      have expand : (S + (m + 1)) ^ 2 = S ^ 2 + (m + 1) ^ 3 :=
+        calc (S + (m + 1)) ^ 2
+            = S ^ 2 + S * 2 * (m + 1) + (m + 1) ^ 2 := by ring
+          _ = S ^ 2 + (m + 1) * m * (m + 1) + (m + 1) ^ 2 := by rw [h]
+          _ = S ^ 2 + (m + 1) ^ 3 := by ring
+      linarith