Formal target: Corpus.Erdos313.erdos_313.variants.primary_pseudoperfect_are_infinite

It is conjectured that the set of primary pseudoperfect numbers is infinite.

Exact formal statement

Set.Infinite.{0} (Set.ofPred.{0} fun n => Corpus.Erdos313.IsPrimaryPseudoperfect n)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record