Milestone 1: Twice the triangular sum

Proved

SumOfCubesPractice.triangleSum_twice

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}(n)=\sum_{k=1}^{n}k$ . Then

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

This gives a multiplication-only expression for twice the triangular sum.

Preamble

import Definitions.Def_SumOfCubesPractice_triangleSum

Formal statement

namespace SumOfCubesPractice

theorem triangleSum_twice (n : ℕ) :
    2 * triangleSum n = n * (n + 1) := by sorry

end SumOfCubesPractice

Source

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

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 $0$ ), twice the sum of all natural numbers $k$ satisfying $1 \le k \le n$ equals $n(n+1)$ : $2\sum_{k=1}^{n} k = n(n+1)$ . The sum and all arithmetic are in the natural numbers; when $n=0$ , the sum is empty and is $0$ , so both sides are $0$ .

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