Number theory
Erdős 313 - primary pseudoperfect are infinite
It is conjectured that the set of primary pseudoperfect numbers is infinite.No one has attempted this yet.
Formal statement
Lean type
{n | Erdos313.IsPrimaryPseudoperfect n}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«313»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos313.erdos_313.variants.primary_pseudoperfect_are_infinite" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/313.lean
- Source type SHA-256
- sha256:41903c46ff6707aac83ac139f030ae58fc308a66a9b0334fdada59ed542b60f0
- Task id
- fc-379fc029-variants-primary-pseudoperfect-are-infinite-a79af02282-formalized-v1
- Task commitment
- sha256:0a69beb4d42abde9996957f46b8fe62fd2a6c3baeae7413000e9492067100156
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.