Non-Power-of-2 Almost Perfect Numbers Conjecture

References:

• Wikipedia
• mathworld

def AlmostPerfectNumbers.AlmostPerfect (n : ℕ) : Prop

A number is almost perfect if the sum of its divisors is equal to $2n - 1$.

Equations

• AlmostPerfectNumbers.AlmostPerfect n = (1 + (ArithmeticFunction.sigma 1) n = 2 * n)

theorem AlmostPerfectNumbers.exists_almost_perfect_not_power_of_two : True ↔ ∃ (n : ℕ), AlmostPerfect n ∧ ¬∃ (k : ℕ), n = 2 ^ k

Non-Power-of-2 Almost Perfect Numbers Conjecture. Does there exist an almost perfect number that is not a power of 2?