Complete characterization of $2$-near perfect numbers with exactly 2 prime factors
Richard Fearon, Henry Foushee, Benjamin Porosoff, Alexander Skula, Joshua Zelinsky, Kyle Zhang
math.NT
Aug 8, 2025 · v3
TL;DR
The main classification of 2-near perfect numbers of the form 2^k p^m is formalized in Lean 4 using Mathlib, with a public repository.
Abstract
A positive integer $n$ is $2$-near perfect} if $σ(n)=2n+d_1+d_2$ for two distinct positive divisors $d_1,d_2$ of $n$. We give a complete classification of $2$-near perfect numbers of the form $2^kp^m$ with $p$ an odd prime and $m\ge3$: every such number belongs to the family $2^k(2^{k+1}-1)^3$, where $p=2^{k+1}-1$ is a Mersenne prime and the omitted divisors are $p$ and $p^2$, and all such numbers are $2$-near perfect. In particular, there are infinitely many $2$-near perfect numbers in this family if and only if there are infinitely many Mersenne primes. Under the standard conjecture that there are infinitely many Mersenne primes, this disproves a conjecture of Aryan, Madhavani, Parikh, Slattery, and Zelinsky that only finitely many such numbers exist. Combined with prior work handling $m\in\{1,2\}$, this yields a complete characterization of all $2$-near perfect numbers with exactly two distinct prime factors.
Problem
A positive integer n is 2-near perfect if σ(n)=2n+d1+d2 for two distinct divisors of n. The open case is numbers of the form 2^k p^m with p an odd prime and m≥3. Aryan et al. conjectured that only finitely many such numbers exist.
Approach
Odd 2-near perfect numbers with two prime factors are first ruled out using bounds on σ(n)/n. The argument then splits on whether 2^{k+1}≥p^2+1 or 2^{k+1}<p^2+1. In each case, divisibility and size constraints on the omitted divisors eliminate the impossible configurations. The main classification is formalized in Lean 4 with Mathlib, and a C++ computational search accompanies it.
Results
Every such number with m≥3 has the form 2^k(2^{k+1}-1)^3, where 2^{k+1}-1 is a Mersenne prime and the omitted divisors are p and p^2. Together with prior work for m∈{1,2}, this completes the characterization for two prime factors and disproves the finiteness conjecture if there are infinitely many Mersenne primes. A side result classifies 2-deficient perfect numbers 2^k p^m with m≠2.
