Sum of cubes identity

Proved

SumOfCubesPractice.cubeSum_eq_triangleSum_sq

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

finite-sumsnumber-theorypractice

For every natural number $n$ , including zero, the sum of the cubes of the first $n$ positive integers equals the square of their sum:

\operatorname{cubeSum}(n)=\operatorname{triangleSum}(n)^2,

where $\operatorname{cubeSum}(n)=\sum_{k=1}^{n}k^3$ and $\operatorname{triangleSum}(n)=\sum_{k=1}^{n}k$ . Empty sums have value zero. This is the main identity of the practice mission.

Preamble

import Definitions.Def_SumOfCubesPractice_triangleSum
import Definitions.Def_SumOfCubesPractice_cubeSum

Formal statement

namespace SumOfCubesPractice

theorem cubeSum_eq_triangleSum_sq (n : ℕ) :
    cubeSum n = triangleSum n ^ 2 := by sorry

end SumOfCubesPractice

Source

Requester-supplied mathematical statement for Sum of Cubes Identity (Practice); no external bibliographic source supplied. Final goal.

Read-back

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

For every natural number $n$ , the sum of the cubes of all natural numbers from $1$ through $n$ , inclusive, equals the square of their sum: $\sum_{k=1}^{n} k^3 = \left(\sum_{k=1}^{n} k\right)^2$ . All sums and arithmetic are in the natural numbers. This includes $n=0$ , when both sums are empty and equal to $0$ , so the equality is $0=0^2$ .

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by hacv16 · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph