Erdős Problem 1052

Reference: erdosproblems.com/1052

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

A proper unitary divisor of $n$ is $d \mid n$ such that $(d, n/d) = 1$ other than $n$.

Equations

• Erdos1052.properUnitaryDivisors n = Finset.filter (fun (d : ℕ) => d ∣ n ∧ d.Coprime (n / d)) (Finset.Ico 1 n)

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 : Set.Finite IsUnitaryPerfect ↔ sorry

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.

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