17. Sum of odd numbers

MediumProofAcademy Pass20 points

oddSum n adds up the first n odd numbers, 1 + 3 + … + (2n − 1). Prove that the result is always n * n.

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Solution.lean

1def oddSum : Nat → Nat

2 | 0 => 0

3 | n + 1 => oddSum n + (2 * n + 1)

4theorem solution (n : Nat) : oddSum n = n * n := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

n:Nat

⊢oddSum n = n * n

ReadyLn 1, Col 1Lean 4

Draft saved in this browser