Erdős problem 1052 · problems.science

All unitary perfect numbers are even.

Sources

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

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.