Solitary Numbers

References:

• Solitary number (Wikipedia)
• Solitary number large clubs (Wikipedia)

def SolitaryNumber.Friendly (m n : ℕ) : Prop

Two positive integers $m$ and $n$ are friendly if they have the same abundancy index, that is $\sigma(m) / m = \sigma(n) / n$, expressed via cross-multiplication to avoid rationals.

Equations

• SolitaryNumber.Friendly m n = (0 < m ∧ 0 < n ∧ (ArithmeticFunction.sigma 1) m * n = (ArithmeticFunction.sigma 1) n * m)

def SolitaryNumber.IsSolitary (n : ℕ) : Prop

A positive integer $n$ is solitary if every friend of $n$ is equal to $n$, i.e. its abundancy class is the singleton $\{n\}$.

Equations

• SolitaryNumber.IsSolitary n = (0 < n ∧ ∀ (m : ℕ), SolitaryNumber.Friendly m n → m = n)

theorem SolitaryNumber.is_ten_solitary : True ↔ IsSolitary 10

Is 10 a solitary number? The smallest positive integer whose solitary status is currently unresolved is $10$, with abundancy index $\sigma(10) / 10 = 9/5$.

theorem SolitaryNumber.infinite_club_exists : True ↔ ∃ (n : ℕ), 0 < n ∧ {m : ℕ | Friendly m n}.Infinite

Existence of an infinite club. A club is an abundancy equivalence class, i.e. the set of all positive integers friendly with a given $n$. It is unknown whether any club is infinite.