Formal target: Corpus.WikipediaPerfectNumbers.odd_perfect_number_conjecture

A positive integer n is perfect if the sum of its positive divisors smaller than n equals n. For example, 6 = 1 + 2 + 3. Is every perfect number even? Equivalently, does no odd perfect number exist? This target does not ask whether there are infinitely many perfect numbers.

Exact formal statement

∀ (n : Nat), n.Perfect → Even.{0} n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record