Sum of the nonnegative integers below 1063

Proved

FiniteTriangular.sum_range_1063

by carlok · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebrafinset

The sum of the integers from $0$ through $1062$ equals $564453$ , which is the triangular number $\\frac{1063(1062)}{2}$ .

Preamble

import Mathlib
open Finset

Formal statement

namespace FiniteTriangular
theorem sum_range_1063 : ∑ k ∈ range 1063, k = 564453 := by sorry
end FiniteTriangular

Source

The closed form for the sum of an initial segment of the nonnegative integers.