Theorem_of_Even_Perfect_Numbers
Provedmersenne-primesnamed-theoremsnumber-theoryperfect-numbersproofwiki
If 2^n - 1 is prime, then 2^(n-1) * (2^n - 1) is a perfect number.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Theorem_of_Even_Perfect_Numbers (n : ℕ) (hp : Nat.Prime (2 ^ n - 1)) : Nat.Perfect (2 ^ (n - 1) * (2 ^ n - 1)) := by sorry
Source