Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Number theory P-amicable-numbers

Amicable numbers

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

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow
Cite 
@misc{cairn-amicable-numbers,
  title        = {Amicable numbers},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/amicable-numbers}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

relatively_prime_amicable. Relatively prime amicable numbers conjecture. Do there exist amicable numbers with ?

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

infinitely_many_amicable. 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

opposite_parity_amicable. Amicable numbers with opposite parity conjecture. Do there exist amicable numbers 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

Two distinct positive integers form an amicable pair if each equals the sum of the proper divisors of the other. Equivalently, is an amicable pair if and , where denotes the sum of all positive divisors of .

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)?

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.AmicableNumbers (3 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem relatively_prime_amicable :
    answer(sorry) ↔ ∃ a b : ℕ, IsAmicable a b ∧ a ≠ b ∧ a.Coprime b
theorem infinitely_many_amicable : type_of% Erdos830.erdos_830.parts.i
theorem opposite_parity_amicable :
    answer(sorry) ↔ ∃ a b : ℕ, IsAmicable a b ∧ (Even a ↔ Odd b)

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.