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 statement3 of 7

FormalConjectures/ErdosProblems/1052.leanErdos1052.isUnitaryPerfect_1463619461864585625600001 lineExact file

1Erdos1052.IsUnitaryPerfect 146361946186458562560000

TestProof 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.