Mathematical Formula

Differenza dei quadrati
Differenza dei quadrati 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.

13 agosto 2026 · L'hai trovato utile?

Altri approcci a Differenza dei quadrati in Lean

Altri modi in cui la nostra community ha risolto questo esercizio
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.