Erdős Problem 469

Reference: erdosproblems.com/469

def Nat.IsSumDivisors (n : ℕ) : Prop

The proposition that n is a sum of distinct proper divisors.

Equations

• n.IsSumDivisors = ∃ S ⊆ n.properDivisors, ∑ d ∈ S, d = n

theorem erdos_469 : (Summable fun (n : ↑{n : ℕ | 0 < n ∧ n.IsSumDivisors ∧ ∀ m < n, m ∣ n → ¬m.IsSumDivisors}) => 1 / ↑↑n) ↔ sorry

Let $A$ be the set of all $n$ such that $n = d_1 + ⋯ + d_k$ with $d_i$ distinct proper divisors of $n$, but this is not true for any $m ∣ n$ with $m < n$. Does: $$ \sum_{n ∈ A} \frac 1 n $$ converge?