--- /dev/null
+++ b/Mathlib/Unsorry/SumRangePowFourClosedForm.lean
@@ -0,0 +1,15 @@
+/-
+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
+
+theorem sum_range_pow_four_closed (n : ℕ) : 30 * (∑ k ∈ Finset.range (n + 1), (k : ℤ) ^ 4) = n * (n + 1) * (2 * n + 1) * (3 * n ^ 2 + 3 * n - 1) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [Finset.sum_range_succ, mul_add, ih]
+    push_cast
+    ring