number-theory · divisors · multiplicative-functions
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.
Why it matters
Even perfect numbers have the Euclid–Euler description in terms of Mersenne primes. The odd case asks whether a completely different kind of divisor balance is possible.
One possible first attack
Rule out odd prime powers: for an odd prime p and a ≥ 1, use 1 + p + … + p^a < 2p^a to show that p^a is not perfect. Keep n = 1 separate. This excludes one family only, not numbers with several distinct prime factors.
Mathematical status
Open (checked 2026-09-11). Ochem and Rao’s published work proves that an odd perfect number, if one exists, exceeds 10^1500; their research page reports subsequent stronger computational bounds. No finite lower bound proves nonexistence. The target is exactly the assertion that every positive perfect natural number is even.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Ochem and Rao, Odd perfect numbers are greater than 10^1500: primary theorem, definition and Euler form (checked 2026-09-11): https://www.lirmm.fr/~ochem/opn/opn.pdf
Authors’ research page: later computational bounds, distinguished from nonexistence (checked 2026-09-11): https://www.lirmm.fr/~ochem/opn/
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/PerfectNumbers.lean
Local target: Corpus.WikipediaPerfectNumbers.odd_perfect_number_conjecture
Source SHA-256: 5619c07d5118b35cb8319dd12d06e5bd6e5af998216a9139bfac22ba53806292
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
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.
No odd prime power p^a (a≥1) is perfect. Uses the divisor-sum characterization and a geometric-sum bound for odd primes. Does not address odd integers with several distinct prime factors.
For p≥2 and a≥1, the partial geometric sum 1+p+…+p^(a-1) is strictly less than p^a.
The natural number 1 is not perfect.
No public records on this page.