Perfect numbers and their relatives

Perfect, multiperfect, odd perfect, abundant, practical, Zumkeller, Giuga, amicable numbers, spoof factorizations, Lehmer's totient problem.

TheoremEuler's theorem on even perfect numbers#✓fully proved

Every even perfect number \(N\) is of the form \(N = 2^{p-1}(2^p - 1)\) for some natural number \(p\) such that \(p\) and \(2^p - 1\) are both prime.

theorem euler_characterization_of_even_perfect_numbers
    (N : ℕ)
    (hN_even : Even N)
    (hN_perfect : Nat.Perfect N) :
    ∃ p : ℕ, Nat.Prime p ∧ Nat.Prime (2 ^ p - 1) ∧
      N = 2 ^ (p - 1) * (2 ^ p - 1)
Sources
  • Paulo J. Almeida and Gabriel Cardoso, "An Extension of the Euclid-Euler Theorem to Certain α-Perfect Numbers," Journal of Integer Sequences 25 (2022), Article 22.8.4, Theorem [Euler] (unlabeled), lines 164–166, https://cs.uwaterloo.ca/journals/JIS/VOL25/Almeida/almeida9.tex

DefinitionExtremely abundant number#✓fully proved

Let \(\sigma(n)\) denote the sum of the positive divisors of \(n\). A natural number \(n\) is extremely abundant if either \(n = 10080\), or \(n > 10080\) and \(\sigma(n) / (n \log \log n) > \sigma(m) / (m \log \log m)\) for every natural number \(m\) with \(10080 \le m < n\), where \(\log\) is the natural logarithm.

public def IsExtremelyAbundantNumber (n : Nat) : Prop :=
  n = 10080 ∨
    (10080 < n ∧
      ∀ m : Nat, 10080 ≤ m → m < n →
        ((ArithmeticFunction.sigma 1 n : Nat) : Real) /
            ((n : Real) * Real.log (Real.log (n : Real))) >
          ((ArithmeticFunction.sigma 1 m : Nat) : Real) /
            ((m : Real) * Real.log (Real.log (m : Real))))

DefinitionGiuga number#✓fully proved

A natural number \(n\) is a Giuga number if it is composite (that is, \(n \ge 2\) and \(n\) is not prime) and \(p\) divides \(n/p - 1\) for every prime divisor \(p\) of \(n\).

public def IsGiugaNumber (n : ℕ) : Prop :=
  2 ≤ n ∧ ¬ Nat.Prime n ∧ ∀ p, Nat.Prime p → p ∣ n → p ∣ (n / p - 1)
Sources

DefinitionPractical number#✓fully proved

A natural number \(n\) is practical if \(n > 0\) and every integer \(m\) with \(1 \le m \le n\) is the sum of a set of distinct positive divisors of \(n\).

public def IsPracticalNumber (n : ℕ) : Prop :=
  0 < n ∧ ∀ m, 1 ≤ m → m ≤ n →
    ∃ s : Finset ℕ, s ⊆ n.divisors ∧ ∑ x ∈ s, x = m
Used by 5
Used byLarge integers as a practical number plus two polygonal numbers · Every positive integer is a practical number plus a triangular number · Practical numbers divisible by neither 3 nor 4 · Products of a practical number with small factors · Exceptions to sums of a practical number and polygonal numbers

TheoremThābit ibn Qurra's theorem#✓fully proved

Let \(n \ge 2\) be a natural number and put \(p = 3 \cdot 2^n - 1\), \(q = 3 \cdot 2^{n-1} - 1\) and \(r = 9 \cdot 2^{2n-1} - 1\). If \(p\), \(q\) and \(r\) are all prime, then \(2^n p q < 2^n r\), the sum of the proper divisors of \(2^n p q\) equals \(2^n r\), and the sum of the proper divisors of \(2^n r\) equals \(2^n p q\); that is, \(2^n p q\) and \(2^n r\) are distinct amicable numbers.

Proof: Following Thabit ibn Qurra's construction as recorded in Dickson, History of the Theory of Numbers, Vol. I, Ch. I, p. 39, and the cited Wikipedia account, compute full divisor sums by multiplicativity and recover the proper-divisor sums by subtracting each number.

theorem thabit_ibn_qurra :
    ∀ (n p q r : ℕ), 2 ≤ n →
      p = 3 * 2 ^ n - 1 →
      q = 3 * 2 ^ (n - 1) - 1 →
      r = 9 * 2 ^ (2 * n - 1) - 1 →
      Nat.Prime p → Nat.Prime q → Nat.Prime r →
      2 ^ n * p * q < 2 ^ n * r ∧
      ∑ d ∈ Nat.properDivisors (2 ^ n * p * q), d = 2 ^ n * r ∧
      ∑ d ∈ Nat.properDivisors (2 ^ n * r), d = 2 ^ n * p * q
Sources
  • https://en.wikipedia.org/wiki/Amicable_numbers#Th%C4%81bit_ibn_Qurra_theorem
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.