Mathematical Formula

Difference of Squares
Difference of Squares in Lean

A possible way to solve this exercise is to use known mathematical formulas:

  • The sum of positive integers up to n, inclusive, is n * (n + 1) / 2. Squaring that sum gives squareOfSum.
  • The sum of the squares of positive integers up to n, inclusive, is n * (n + 1) * (2 * n + 1) / 6.
def sumFirstNPositive (n : Nat) : Nat :=
    n * (n + 1) / 2

def squareOfSum (number : Nat) : Nat :=
    (sumFirstNPositive number) ^ 2

def sumOfSquares (number : Nat) : Nat :=
    (number * (number + 1) * (2 * number + 1)) / 6

def differenceOfSquares (number : Nat) : Nat :=
    (squareOfSum number) - (sumOfSquares number)

This is probably the most efficient approach, since the problem reduces to a few constant multiplications and divisions, whereas the other approaches are O(n). On the other hand, the solution becomes more opaque because these formulas are not obvious from the structure of the problem. They require previous knowledge or further research.

13th Aug 2026 · Found it useful?

Other Approaches to Difference of Squares in Lean

Other ways our community solved this exercise
def sumN (n : Nat) (acc : Nat) : Nat :=
    if n = 0 then acc else sumN (n - 1) (acc + n)

def squareOfSum (number : Nat) : Nat :=
    (sumN number 0) ^ 2

def sumOfSquares (number : Nat) (acc := 0) : Nat :=
    if n = 0 then acc else sumSquareN (n - 1) (acc + (n ^ 2))
Recurse Over Numbers

recurse over all numbers to sum them up. 

def squareOfSum (number : Nat) : Nat :=
    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
    sum ^ 2

def sumOfSquares (number : Nat) : Nat :=
    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
Folding Over Range

use a fold to sum all numbers in a range.