1. FormalConjectures
  2. ErdosProblems
  3. «1052»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 1052

Reference: erdosproblems.com/1052

namespace Erdos1052

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

def properUnitaryDivisors (n : ℕ) : Finset ℕ := {d ∈ Finset.Ico 1 n | d ∣ n ∧ d.Coprime (n / d)}

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

def IsUnitaryPerfect (n : ℕ) : Prop := ∑ i ∈ properUnitaryDivisors n, i = n ∧ 0 < n

Are there only finitely many unitary perfect numbers?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_1052 : answer(sorry) ↔ {n | IsUnitaryPerfect n}.Finite := ⊢ True ↔ {n | IsUnitaryPerfect n}.Finite All goals completed! 🐙

All unitary perfect numbers are even.

Formal proof linked here provided by AlphaProof.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mzhorvath1/formal-conjectures/blob/b70a2ddf5e55f743aac9d4f4a907786b39bc9807/FormalConjectures/ErdosProblems/1052.lean#L46"] theorem declaration uses 'sorry'even_of_isUnitaryPerfect (n : ℕ) (hn : IsUnitaryPerfect n) : Even n := n:ℕhn:IsUnitaryPerfect n⊢ Even n All goals completed! 🐙 @[category test, AMS 11] theorem isUnitaryPerfect_6 : IsUnitaryPerfect 6 := ⊢ IsUnitaryPerfect 6 ⊢ ∑ i ∈ Finset.Ico 1 6 with i ∣ 6 ∧ i.Coprime (6 / i), i = 6 All goals completed! 🐙 @[category test, AMS 11] theorem isUnitaryPerfect_60 : IsUnitaryPerfect 60 := ⊢ IsUnitaryPerfect 60 ⊢ ∑ i ∈ Finset.Ico 1 60 with i ∣ 60 ∧ i.Coprime (60 / i), i = 60 All goals completed! 🐙 @[category test, AMS 11] theorem isUnitaryPerfect_90 : IsUnitaryPerfect 90 := ⊢ IsUnitaryPerfect 90 ⊢ ∑ i ∈ Finset.Ico 1 90 with i ∣ 90 ∧ i.Coprime (90 / i), i = 90 All goals completed! 🐙 @[category test, AMS 11] theorem declaration uses 'sorry'isUnitaryPerfect_87360 : IsUnitaryPerfect 87360 := ⊢ IsUnitaryPerfect 87360 -- TODO: Find a quicker proof. This one is too slow. All goals completed! 🐙 @[category test, AMS 11, formal_proof using formal_conjectures at "https://github.com/Sanexxxx777/formal-conjectures/blob/be8aed15e8888a08bbe723170698e26c046412a4/FormalConjectures/ErdosProblems/1052.lean#L346"] theorem declaration uses 'sorry'isUnitaryPerfect_146361946186458562560000 : IsUnitaryPerfect 146361946186458562560000 := ⊢ IsUnitaryPerfect 146361946186458562560000 All goals completed! 🐙 end Erdos1052