Documentation

Archive.Wiedijk100Theorems.PerfectNumbers

Perfect Numbers #

This file proves Theorem 70 from the 100 Theorems List.

The theorem characterizes even perfect numbers.

Euclid proved that if 2 ^ (k + 1) - 1 is prime (these primes are known as Mersenne primes), then 2 ^ k * 2 ^ (k + 1) - 1 is perfect.

Euler proved the converse, that if n is even and perfect, then there exists k such that n = 2 ^ k * 2 ^ (k + 1) - 1 and 2 ^ (k + 1) - 1 is prime.

References #

https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem

Euclid's theorem that Mersenne primes induce perfect numbers

theorem Theorems100.Nat.eq_two_pow_mul_odd {n : } (hpos : 0 < n) :
k m, n = 2 ^ k * m ¬Even m

Perfect Number Theorem: Euler's theorem that even perfect numbers can be factored as a power of two times a Mersenne prime.

The Euclid-Euler theorem characterizing even perfect numbers