Nielsen: $N < 2^{4^{\omega(N)}}$ for an odd perfect number

Proved

OddPerfectNumber.nielsen_upper_bound

by Gabewhigham · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-sumsnumber-theoryopen-problemperfect-numbers

Nielsen's upper bound (2003). If $N$ is an odd perfect number with $k = \omega(N)$ distinct prime divisors, then

N < 2^{4^{k}}.

The bound is doubly exponential in $k$ , and it is the first result of its type: it makes the set of odd perfect numbers with a fixed number of distinct prime factors finite, hence in principle decidable by a finite (if astronomically large) computation. Combined with a lower bound on $\omega(N)$ it constrains the search region used in the computational work on the problem. Nielsen later sharpened the bound to $N < 2^{4^{k} - 2^{k}}$ ; a formalization of the sharper statement also settles this milestone.

Formalized with $\omega(N)$ as N.primeFactors.card.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber

theorem nielsen_upper_bound (n : ℕ) (hn : Nat.Perfect n) (hodd : Odd n) :
    n < 2 ^ (4 ^ n.primeFactors.card) := by
  sorry

end OddPerfectNumber

Source

P. P. Nielsen, An upper bound for odd perfect numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14, Theorem 1.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by Gabewhigham · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Nielsen: N<24ω(N)N < 2^{4^{\omega(N)}}N<24ω(N) for an odd perfect number

Nielsen: $N < 2^{4^{\omega(N)}}$ for an odd perfect number