Skip to content

Erdős problem 469

Start work

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/469.lean

Formal Conjectures

FormalConjectures/ErdosProblems/469.leanErdos469.erdos_4691 lineExact file
True ↔ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:469
  • PLBY Lean proofsErdosProblems.Erdos469

Reported activity

Reported by these sources. Not reviewed here.

  • argument

    VibeMathed

    Machine
    GPT-5.6 Sol Ultra, Claude Fable 5
    People
    Zachary J. Lewis
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry