Odd Perfect Number Conjecture

Reference: Wikipedia

The Odd Perfect Number Conjecture states that all perfect numbers are even. 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. The conjecture states that this is not a coincidence - there are no odd perfect numbers.

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

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

theorem 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"

theorem 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 ≡ 1 (mod 4), α ≡ 1 (mod 4), and p ∤ m.

Reference: Euler's theorem on odd perfect numbers