Amicable numbers

Two distinct positive integers form an amicable pair if each equals the sum of the proper divisors of the other. Equivalently, $(a, b)$ is an amicable pair if $\sigma(a) = a + b$ and $\sigma(b) = a + b$, where $\sigma(n)$ denotes the sum of all positive divisors of $n$.

Several open problems about amicable numbers are formalised here:

• Do there exist relatively prime amicable numbers?
• Are there infinitely many amicable pairs?
• Do there exist amicable numbers with opposite parity (one even, one odd)?

References:

• Wikipedia
• MathWorld
• OEIS A063990

theorem AmicableNumbers.amicable_220_284 : IsAmicable 220 284

The classic amicable pair $(220, 284)$.

theorem AmicableNumbers.IsAmicable.symm {a b : ℕ} (h : IsAmicable a b) : IsAmicable b a

IsAmicable is symmetric.

theorem AmicableNumbers.relatively_prime_amicable : True ↔ ∃ (a : ℕ) (b : ℕ), IsAmicable a b ∧ a ≠ b ∧ a.Coprime b

Relatively prime amicable numbers conjecture. Do there exist amicable numbers $(a, b)$ with $\gcd(a, b) = 1$?

All known amicable pairs share a common factor. It is an open question whether a pair of relatively prime amicable numbers can exist.

Reference: Wikipedia

theorem AmicableNumbers.infinitely_many_amicable : True ↔ {(a, b) : ℕ × ℕ | IsAmicable a b}.Infinite

Infinitely many amicable numbers conjecture.

Are there infinitely many pairs of amicable numbers?

While many amicable pairs are known, it remains open whether there are infinitely many.

Reference: Wikipedia, erdosproblems.com/830

theorem AmicableNumbers.opposite_parity_amicable : True ↔ ∃ (a : ℕ) (b : ℕ), IsAmicable a b ∧ (Even a ↔ Odd b)

Amicable numbers with opposite parity conjecture. Do there exist amicable numbers $(a, b)$ where one is even and the other is odd?

All known amicable pairs are either both even or both odd. It is widely believed that mixed-parity amicable pairs do not exist, but this remains open.

Reference: Wikipedia