Number theory

Perfect numbers: 6 and 28

Compute divisors, sum them, and check the first two perfect numbers.

-- Top 100 #70: Perfect numbers: 6 and 28
-- History: c. 300 BCE · Euclid’s construction.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The proper divisors of 6 are 1, 2, and 3, which add back to 6.
-- Scope: Checks the defining divisor-sum property at 6 and 28. Euclid’s general construction and Euler’s converse are not proved.
-- Source: https://lurch.plus/100/

def properDivisors (n : Nat) : List Nat :=
  (List.range n).filter fun d => d > 0 && n % d == 0

def divisorSum (n : Nat) := (properDivisors n).foldl (· + ·) 0

example : divisorSum 6 = 6 := by decide
example : divisorSum 28 = 28 := by decide

#eval properDivisors 28
#eval divisorSum 28

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

c. 300 BCE · Euclid’s construction

The proper divisors of 6 are 1, 2, and 3, which add back to 6.

Checks the defining divisor-sum property at 6 and 28. Euclid’s general construction and Euler’s converse are not proved.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

[1, 2, 4, 7, 14]
28

Exercise

Evaluate divisorSum 496. Compare the result with the input.