# mathlib3documentation

mathlib-archive / wiedijk_100_theorems.perfect_numbers

# Perfect Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 theorems_100.nat.eq_two_pow_mul_odd {n : } (hpos : 0 < n) :
(k m : ), n = 2 ^ k * m ¬even m
theorem theorems_100.nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : } (ev : even n) (perf : n.perfect) :
(k : ), nat.prime (mersenne (k + 1)) n = 2 ^ k * mersenne (k + 1)

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

theorem theorems_100.nat.even_and_perfect_iff {n : } :
even n n.perfect (k : ), nat.prime (mersenne (k + 1)) n = 2 ^ k * mersenne (k + 1)

The Euclid-Euler theorem characterizing even perfect numbers