Multiperfect numbers

Definition\(k\)-perfect numbers#✓fully proved

For natural numbers \(k\) and \(n\), the number \(n\) is \(k\)-perfect when \(n > 0\) and \(\sigma(n) = kn\), where \(\sigma(n)\) is the sum of the positive divisors of \(n\).

def IsKPerfect (k n : ℕ) : Prop :=
  0 < n ∧ (ArithmeticFunction.sigma 1) n = k * n
Used by 2
Used byPerfect numbers are the \(2\)-perfect numbers · The parameter of a \(k\)-perfect number is positive

TheoremThe parameter of a \(k\)-perfect number is positive#✓fully proved

For natural numbers \(k\) and \(n\), if \(n\) is \(k\)-perfect, then \(k > 0\).

theorem IsKPerfect.pos_k {k n : ℕ} (h : IsKPerfect k n) : 0 < k
Uses 1
Statement uses\(k\)-perfect numbers

TheoremPerfect numbers are the \(2\)-perfect numbers#✓fully proved

A natural number \(n\) is \(2\)-perfect if and only if it is perfect, that is, \(n > 0\) and the sum of the proper divisors of \(n\) equals \(n\).

theorem isKPerfect_two_iff (n : ℕ) : IsKPerfect 2 n ↔ n.Perfect
Uses 1
Statement uses\(k\)-perfect numbers

TheoremTwo Pillai equations in powers of two and three#✓fully proved

For natural numbers \(a\) and \(b\), the integer equation \(2^a - 3^b = -1\) holds if and only if \((a, b) = (1, 1)\) or \((a, b) = (3, 2)\). For natural numbers \(a\), \(b\) and \(c\), the integer equation \(2^a - 3^b = 2^c - 1\) holds if and only if \((a, b, c) = (2, 1, 1)\), or \((a, b, c) = (4, 2, 3)\), or \(b = 0\) and \(c = a\).

public theorem pillai_equations_two_pow_three_pow :
    (∀ a b : ℕ, (2 : ℤ) ^ a - 3 ^ b = -1 ↔
        (a = 1 ∧ b = 1) ∨ (a = 3 ∧ b = 2)) ∧
      (∀ a b c : ℕ, (2 : ℤ) ^ a - 3 ^ b = 2 ^ c - 1 ↔
        (a = 2 ∧ b = 1 ∧ c = 1) ∨ (a = 4 ∧ b = 2 ∧ c = 3) ∨
        (b = 0 ∧ c = a))
Sources

TheoremSteuerwald's theorem on 3-perfect numbers#✓fully proved

Let \(N\), \(a\), \(b\) and \(m\) be natural numbers with \(N = 2^a 3^b m\), \(a \ge 1\), \(b \ge 1\), and \(m\) coprime to \(6\). If \(\sigma(N) = 3N\), where \(\sigma(N)\) is the sum of the divisors of \(N\), then either \(a = 1\) and \(b \ne 1\), or \(a \ne 1\) and \(b = 1\).

public theorem steuerwald_three_perfect_exponents
    (N a b m : ℕ)
    (hperfect : ArithmeticFunction.sigma 1 N = 3 * N)
    (hform : N = 2 ^ a * 3 ^ b * m)
    (ha : 1 ≤ a) (hb : 1 ≤ b)
    (hcoprime : Nat.Coprime 6 m) :
    (a = 1 ∧ b ≠ 1) ∨ (a ≠ 1 ∧ b = 1)
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL25/Almeida/almeida9.tex, lines 210-219.
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.