Documentation

FormalConjectures.Wikipedia.PerfectNumbers

Perfect numbers #

A perfect number is a positive integer that equals the sum of its proper divisors (i.e., all its positive divisors excluding the number itself).

For example, 6 is perfect because its proper divisors are 1, 2, and 3, and 1 + 2 + 3 = 6. Similarly, 28 is perfect because 1 + 2 + 4 + 7 + 14 = 28.

All known perfect numbers are even. Several open problems about perfect numbers are formalised here:

References:

source
theorem PerfectNumbers.infinitely_many_perfect :
sorry ↔ {n : ℕ | n.Perfect}.Infinite

Infinitely many perfect numbers conjecture. Are there infinitely many perfect numbers?

Reference: Wikipedia

source
theorem PerfectNumbers.infinitely_many_even_perfect :
sorry ↔ {n : ℕ | n.Perfect ∧ Even n}.Infinite

Infinitely many even perfect numbers conjecture. Are there infinitely many even perfect numbers?

This is equivalent to asking whether there are infinitely many Mersenne primes, since by the Euclid–Euler theorem an even number is perfect if and only if it has the form $2^{p-1}(2^p - 1)$ where $2^p - 1$ is a Mersenne prime.

Reference: Wikipedia

source
theorem PerfectNumbers.odd_perfect_number_conjecture (n : ℕ) (hn : n.Perfect) :
Even n

Odd Perfect Number Conjecture. The Odd Perfect Number Conjecture states that all perfect numbers are even.

Reference: Wikipedia

source
theorem PerfectNumbers.odd_perfect_number.lower_bound (n : ℕ) (hn : Odd n) (hp : n.Perfect) :
n > 10 ^ 1500 ∧ n.primeFactorsList.length ≥ 101

A known result: If an odd perfect number exists, it must be greater than $10^{1500}$ and must have at least 101 prime factors (including multiplicities).

Reference: Pascal Ochem, Michaël Rao (2012). "Odd perfect numbers are greater than 10^1500"

source
theorem PerfectNumbers.odd_perfect_number.euler_form (n : ℕ) (hn : Odd n) (hp : n.Perfect) :
∃ (p : ℕ) (m : ℕ) (α : ℕ), Nat.Prime p ∧ ↑p ≡ 1 [ZMOD 4] ∧ ↑α ≡ 1 [ZMOD 4] ∧ ¬p ∣ m ∧ n = p ^ α * m ^ 2

A known result: If an odd perfect number exists, it must be of the form $p^α * m^2$ where $p$ is prime, $p \equiv 1 \pmod{4}$, $\alpha \equiv 1 \pmod{4}$, and $p \nmid m$.

Reference: Euler's theorem on odd perfect numbers