Mathematical Formula

Diferença de quadrados
Diferença de quadrados em 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 de agosto de 2026 · Achou útil?

Outras abordagens para Diferença de quadrados em Lean

Outras maneiras como a nossa comunidade resolveu este exercício
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.