Erdős problem 1052

All unitary perfect numbers are even.

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1052.lean

Retained formal statement2 of 7

All unitary perfect numbers are even.

Formal proof linked here provided by AlphaProof.

FormalConjectures/ErdosProblems/1052.leanErdos1052.even_of_isUnitaryPerfect1 lineExact file

1∀ (n : ℕ), Erdos1052.IsUnitaryPerfect n → Even n

SolvedProof has a holeformal conjecturesexternal proof

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