Warmups · warm-up

mediumknown result, no worker yet

Gauss's formula, doubled

Theorem · gauss_sum

Gauss's formula, doubled: 2⋅(0+1+⋯+n)=n(n+1)2 \cdot (0 + 1 + \dots + n) = n (n + 1).

Formal statement · Lean 4.lean
theorem gauss_sum (n : Nat) : 2 * ((List.range (n + 1)).foldl (· + ·) 0) = n * (n + 1) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗