Sum of cubes

Definition

SumOfCubesPractice_cubeSum

by hacv16 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-sumsnumber-theorypractice

For every natural number $n$ , define

\operatorname{cubeSum}(n)=\sum_{k=1}^{n}k^3.

The sum includes both endpoints and is zero when $n=0$ . This function represents the sum on the left side of the main identity.

Definition code

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Order.Interval.Finset.Nat

open scoped BigOperators

namespace SumOfCubesPractice

def cubeSum (n : ℕ) : ℕ :=
  ∑ k ∈ Finset.Icc 1 n, k ^ 3

end SumOfCubesPractice

Source

Requester-supplied mathematical statement for Sum of Cubes Identity (Practice); no external bibliographic source supplied. Definitions: cubeSum.

Read-back

What the Lean code literally says, in plain math · Codex, based on GPT-6 (exact model identifier unavailable)

The function $\operatorname{cubeSum}:\mathbb{N}\to\mathbb{N}$ is defined for every natural number $n$ by $\operatorname{cubeSum}(n)=\sum_{k\in\mathbb{N},\,1\le k\le n}k^3$ , the sum of the cubes of all natural numbers from $1$ through $n$ , including both endpoints. In particular, $n=0$ is allowed, in which case the index set is empty and $\operatorname{cubeSum}(0)=0$ .

View graph