Motivation

A positive integer is perfect when it equals the sum of its proper divisors: $6 = 1 + 2 + 3$, $28 = 1 + 2 + 4 + 7 + 14$, then $496$, $8128$, and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.

The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if $2^p - 1$ is prime then $2^{p-1}(2^p - 1)$ is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.

A timeline of what is actually proved about a hypothetical odd perfect number $N$:

• Euler (published posthumously in 1849): $N = p^k m^2$ with $p$ prime, $p \equiv k \equiv 1 \pmod 4$, and $p \nmid m$. In particular $N$ is not a perfect square.
• Servais (1887), Sylvester (1888): lower bounds on the number $\omega(N)$ of distinct prime divisors; Sylvester obtained $\omega(N) \ge 5$, and $\omega(N) \ge 8$ when $3 \nmid N$.
• Touchard (1953): $N \equiv 1 \pmod{12}$ or $N \equiv 9 \pmod{36}$. Shorter proofs were later given by Satyanarayana (1959) and Holdener (2002).
• Chein (1979) and Hagis (1980), independently: $\omega(N) \ge 8$; Nielsen (2007): $\omega(N) \ge 9$; Nielsen (2015): $\omega(N) \ge 10$.
• Nielsen (2003): an upper bound in terms of $\omega$, namely $N < 2^{4^{\omega(N)}}$ — the first bound of its kind, later sharpened by Nielsen himself.
• Ochem–Rao (2012): $N > 10^{1500}$; Ochem–Rao (2014): $N$ has at least $101$ prime factors counted with multiplicity.

None of these results, alone or together, rules out an odd perfect number.

Setting

For $n \ge 1$ write $\sigma(n) = \sum_{d \mid n} d$ for the sum of all positive divisors of $n$. Then $n$ is perfect exactly when

$$\sigma(n) = 2n,$$

equivalently when the divisors of $n$ other than $n$ itself sum to $n$. The function $\sigma$ is multiplicative: $\sigma(ab) = \sigma(a)\sigma(b)$ whenever $\gcd(a,b) = 1$, and $\sigma(p^a) = 1 + p + \cdots + p^a$ for a prime power. The quantity $\sigma(n)/n$ is the abundancy index of $n$, so a perfect number is one of abundancy index exactly $2$.

Write $\omega(n)$ for the number of distinct prime divisors of $n$. In Lean, $\omega(n)$ is n.primeFactors.card, and perfection is Mathlib's Nat.Perfect n, which unfolds to ∑ i ∈ n.properDivisors, i = n ∧ 0 < n — the positivity clause is part of the definition, so $n = 0$ is not perfect.

Formalization targets

Goal

$$\forall n \in \mathbb{N}, \quad \sigma(n) = 2n \ \Longrightarrow\ 2 \mid n.$$

Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.

Milestones

The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number $N$:

$$N = p^k m^2, \quad p \text{ prime}, \quad p \equiv k \equiv 1 \ (\mathrm{mod}\ 4), \quad p \nmid m \qquad \text{(Euler)}$$ $$N \text{ is not a perfect square} \qquad \text{(Euler)}$$ $$\omega(N) \ge 3, \qquad \omega(N) \ge 5 \qquad \text{(Servais, Sylvester)}$$ $$N \equiv 1 \ (\mathrm{mod}\ 12) \quad \text{or} \quad N \equiv 9 \ (\mathrm{mod}\ 36) \qquad \text{(Touchard)}$$ $$N < 2^{4^{\omega(N)}} \qquad \text{(Nielsen)}$$

Significance

The result itself. A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be $2^{p-1}(2^p-1)$ for a Mersenne prime $2^p - 1$. A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than $1500$ decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of $\sigma$, and about the multiperfect numbers.

Formalizing it. Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (Archive/Wiedijk100Theorems/PerfectNumbers.lean, as Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect and Theorems.perfect_iff_even_and_mersenne), and the main library carries the divisor-sum API around Nat.Perfect in Mathlib/NumberTheory/Divisors.lean, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing $\sigma$-arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of $\sigma$ on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.

Difficulty

The obvious approach — take Euler's form $N = p^k m^2$ and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation $\sigma(N) = 2N$ has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing $\omega$ weakens the constraints rather than strengthening them, which is why the lower bounds on $\omega$ have advanced by one prime factor per decade at very high computational cost. The upper bound $N < 2^{4^{\omega(N)}}$ makes the search space finite for each fixed $\omega$, but astronomically so.

Formalization scope

The development is stated over ℕ with Mathlib's Nat.Perfect, so positivity is built into the hypothesis and no separate 0 < n assumption appears. Oddness is Odd n, the number of distinct prime divisors is n.primeFactors.card, and Euler's form is stated with explicit residues p % 4 = 1, k % 4 = 1, together with ¬ p ∣ m and n = p ^ k * m ^ 2. No custom definitions are introduced; everything rests on Mathlib's Nat.sigma / Nat.Perfect API.

One caution on the shape of the milestones. Each is stated conditionally, for an $n$ assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved unconditionally in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.

Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for $\sigma$ on odd numbers. Sharper published bounds — larger values of $\omega$, the improved Nielsen bound $N < 2^{4^{\omega(N)} - 2^{\omega(N)}}$, the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.

Selected references

• L. Euler, De numeris amicabilibus, Commentationes arithmeticae 2 (1849), 627–636.
• J. J. Sylvester, Sur les nombres parfaits, Comptes Rendus de l'Académie des Sciences CVI (1888), 403–405.
• J. Touchard, On prime numbers and perfect numbers, Scripta Mathematica 19 (1953), 35–39.
• J. A. Holdener, A theorem of Touchard on the form of odd perfect numbers, American Mathematical Monthly 109 (2002), 661–663.
• P. P. Nielsen, An upper bound for odd perfect numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14.
• P. P. Nielsen, Odd perfect numbers have at least nine distinct prime factors, Mathematics of Computation 76 (2007), 2109–2126.
• P. P. Nielsen, Odd perfect numbers, Diophantine equations, and upper bounds, Mathematics of Computation 84 (2015), 2549–2567.
• P. Ochem and M. Rao, Odd perfect numbers are greater than $10^{1500}$, Mathematics of Computation 81 (2012), 1869–1877.
• P. Ochem and M. Rao, On the number of prime factors of an odd perfect number, Mathematics of Computation 83 (2014), 2435–2439.
• Overview and further pointers: https://en.wikipedia.org/wiki/Perfect_number