Betrothed numbers

References:

• Wikipedia
• OEIS A005276

structure BetrothedNumbers.IsBetrothed (m n : ℕ) : Prop

Two natural numbers $m$ and $n$ are betrothed (or quasi-amicable) if $\sigma(m) = \sigma(n) = m + n + 1$, where $\sigma$ is the sum-of-divisors function. Equivalently, the sum of the proper divisors of $m$ equals $n + 1$, and the sum of the proper divisors of $n$ equals $m + 1$.

• left : (ArithmeticFunction.sigma 1) m = m + n + 1
• right : (ArithmeticFunction.sigma 1) n = m + n + 1

theorem BetrothedNumbers.isBetrothed_iff (m n : ℕ) : IsBetrothed m n ↔ (ArithmeticFunction.sigma 1) m = m + n + 1 ∧ (ArithmeticFunction.sigma 1) n = m + n + 1

theorem BetrothedNumbers.betrothed_48_75 : IsBetrothed 48 75

The smallest known betrothed pair $(48, 75)$.

theorem BetrothedNumbers.IsBetrothed.symm {m n : ℕ} (h : IsBetrothed m n) : IsBetrothed n m

IsBetrothed is symmetric.

theorem BetrothedNumbers.same_parity_betrothed : sorry ↔ ∃ (m : ℕ) (n : ℕ), IsBetrothed m n ∧ (Even m ↔ Even n)

Same parity betrothed numbers conjecture. Do there exist betrothed numbers $(m, n)$ where both have the same parity (both even or both odd)?

All known betrothed pairs consist of one even and one odd number.

theorem BetrothedNumbers.infinitely_many_betrothed : sorry ↔ {p : ℕ × ℕ | p.1 < p.2 ∧ IsBetrothed p.1 p.2}.Infinite

Infinitude of betrothed numbers conjecture. Are there infinitely many betrothed number pairs?