Erdős Problem 1052

Reference: erdosproblems.com/1052

def Erdos1052.properUnitaryDivisors (n : ℕ) : Finset ℕ

A proper unitary divisor of $n$ is a divisor $d$ of $n$ such that $d$ is coprime to $n/d$, and $d < n$.

Equations

• Erdos1052.properUnitaryDivisors n = {d ∈ Finset.Ico 1 n | d ∣ n ∧ d.Coprime (n / d)}

def Erdos1052.IsUnitaryPerfect (n : ℕ) : Prop

A number $n > 0$ is a unitary perfect number if it is the sum of its proper unitary divisors.

Equations

• Erdos1052.IsUnitaryPerfect n = (∑ i ∈ Erdos1052.properUnitaryDivisors n, i = n ∧ 0 < n)

theorem Erdos1052.erdos_1052 : True ↔ {n : ℕ | IsUnitaryPerfect n}.Finite

Are there only finitely many unitary perfect numbers?

theorem Erdos1052.even_of_isUnitaryPerfect (n : ℕ) (hn : IsUnitaryPerfect n) : Even n

All unitary perfect numbers are even.

Formal proof linked here provided by AlphaProof.

theorem Erdos1052.isUnitaryPerfect_6 : IsUnitaryPerfect 6

theorem Erdos1052.isUnitaryPerfect_60 : IsUnitaryPerfect 60

theorem Erdos1052.isUnitaryPerfect_90 : IsUnitaryPerfect 90

theorem Erdos1052.isUnitaryPerfect_87360 : IsUnitaryPerfect 87360

theorem Erdos1052.isUnitaryPerfect_146361946186458562560000 : IsUnitaryPerfect 146361946186458562560000