Milestone 2: Successive triangular squares

Proved

SumOfCubesPractice.triangleSum_sq_succ

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

finite-sumsnumber-theorypractice

Let $n$ be any natural number, including zero, and let $\operatorname{triangleSum}(m)=\sum_{k=1}^{m}k$ for every natural number $m$ . Then

\operatorname{triangleSum}(n+1)^2=\operatorname{triangleSum}(n)^2+(n+1)^3.

This specifies the increment in the square of the triangular sum between consecutive inputs.

Preamble

import Definitions.Def_SumOfCubesPractice_triangleSum

Formal statement

namespace SumOfCubesPractice

theorem triangleSum_sq_succ (n : ℕ) :
    triangleSum (n + 1) ^ 2 = triangleSum n ^ 2 + (n + 1) ^ 3 := by sorry

end SumOfCubesPractice

Source

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

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$ , including $n=0$ , the square of the sum of all natural numbers from $1$ through $n+1$ , inclusive, equals the square of the sum of all natural numbers from $1$ through $n$ , inclusive, plus the cube of $n+1$ : $\left(\sum_{k=1}^{n+1} k\right)^2=\left(\sum_{k=1}^{n} k\right)^2+(n+1)^3$ . All sums, powers, and arithmetic are in the natural numbers; when $n=0$ , the sum from $1$ through $n$ is empty and equals $0$ , so the asserted equality is $1^2=0^2+1^3$ .

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