Erdős problem 469 · problems.science

Does the sum of the reciprocals of all primitive pseudoperfect numbers converge?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

469.lean

Retained formal statement1 of 1

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?

Yes: the sum converges. This was proved by Lewis [Le25], whose proof has been formalized in Lean.

FormalConjectures/ErdosProblems/469.leanErdos469.erdos_4691 lineExact file

1True ↔ Summable fun n => 1 / ↑↑n

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science