Pseudoperfect numbers

DefinitionPrimitive pseudoperfect numbers#✓fully proved

A natural number \(n\) lies in \(A\), the set of primitive pseudoperfect numbers, when \(n > 0\), \(n\) is pseudoperfect (it is positive and equal to the sum of some set of distinct proper divisors of itself), and no proper divisor of \(n\) (a divisor \(m \mid n\) with \(m < n\)) is pseudoperfect.

def InA (n : Nat) : Prop :=
  0 < n ∧ Nat.Pseudoperfect n ∧
    ∀ m, m ∣ n → m < n → ¬Nat.Pseudoperfect m

Used by 1

Used byErdős Problem 469 (statement)

DefinitionErdős Problem 469 (statement)#✓fully proved

The proposition that the reciprocals of the primitive pseudoperfect numbers have finite sum: the family \((1/n)\), indexed by the natural numbers \(n\) that are primitive pseudoperfect, is summable in \(\mathbb{R}\). Here \(n\) is pseudoperfect if \(n > 0\) and \(n\) is the sum of some set of distinct proper divisors of \(n\), and primitive pseudoperfect if moreover no proper divisor of \(n\) is pseudoperfect.

def conjecture : Prop :=
  Summable (fun a : {n : Nat // InA n} => (1 : Real) / (a.val : Real))

Sources

[EP-469].

Uses 1 · Used by 1

Statement usesPrimitive pseudoperfect numbers

Used byReciprocals of primitive pseudoperfect numbers have finite sum

TheoremReciprocals of primitive pseudoperfect numbers have finite sum#●ready to prove

Call a natural number \(n\) pseudoperfect if \(n > 0\) and \(n\) is the sum of some set of distinct proper divisors of \(n\), and primitive pseudoperfect if moreover no proper divisor of \(n\) is pseudoperfect. Then the family \((1/n)\), indexed by the primitive pseudoperfect numbers \(n\), is summable in \(\mathbb{R}\), that is, the sum of \(1/n\) over all primitive pseudoperfect numbers \(n\) is finite.

This is Erdős Problem 469, resolved true.

public theorem_wanted conjecture_holds : conjecture

Sources

plby/lean-proofs (2026), https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos469.lean.

Uses 1

Statement usesErdős Problem 469 (statement)

DefinitionErdős Problem 825#✓fully proved

Write \(\sigma(n)\) for the sum of the positive divisors of a positive integer \(n\), and call \(n\) pseudoperfect if \(n\) is the sum of the elements of some set of proper divisors of \(n\). The statement is the conjunction of two claims: there is a real \(C > 0\) such that every positive integer \(n\) with \(\sigma(n) > Cn\) is pseudoperfect, and every real \(C > 0\) with this property satisfies \(C > 2\).

def conjecture : Prop :=
  (∃ (C : ℝ) (_ : C > 0),
    ∀ (n) (_ : σ 1 n > C * n),
      Nat.Pseudoperfect n) ∧
  (∀ (C : ℝ), 0 < C →
    (∀ (n : ℕ) (_ : σ 1 n > C * n),
      Nat.Pseudoperfect n) →
    2 < C)

Used by 1

Used byErdős Problem 825 is true

TheoremErdős Problem 825 is true#●ready to prove

Write \(\sigma(n)\) for the sum of the positive divisors of a positive integer \(n\), and call \(n\) pseudoperfect if \(n\) is the sum of the elements of some set of proper divisors of \(n\). Then there is a real \(C > 0\) such that every positive integer \(n\) with \(\sigma(n) > Cn\) is pseudoperfect, and every real \(C > 0\) with this property satisfies \(C > 2\).

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  (∃ (C : ℝ) (_ : C > 0),
    ∀ (n) (_ : σ 1 n > C * n),
      Nat.Pseudoperfect n) ∧
  (∀ (C : ℝ), 0 < C →
    (∀ (n : ℕ) (_ : σ 1 n > C * n),
      Nat.Pseudoperfect n) →
    2 < C)

WantedExt/NumberTheory/ErdosProblem825Wanted.lean:35

Sources

Daniel Larsen, Sufficiently abundant numbers are pseudoperfect, https://github.com/Larsen-Daniel/Erdos-825/blob/18411fce83ce49ee0adbb628de04603e003004f5/825.pdf.

Uses 1

Statement usesErdős Problem 825

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.