AmicableNumbers.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 3 contain sorry, 0 declared as axioms

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:

Imports (2)

theorem AmicableNumbers.amicable_220_284 The classic amicable pair $(220, 284)$ line 47 source
Source documentation
The classic amicable pair $(220, 284)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsAmicable, OfNat.ofNat, Nat
Proof uses: IsAmicable.mk, of_decide_eq_true, Eq, ArithmeticFunction, ArithmeticFunction.sigma, HAdd.hAdd, id, Bool, Decidable.decide, Bool.true, Eq.refl, Ne
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem amicable_220_284 : IsAmicable 220 284 := by
…
```
Mentions: IsAmicable
theorem AmicableNumbers.IsAmicable.symm IsAmicable is symmetric line 52 source
Source documentation
IsAmicable is symmetric.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsAmicable
Proof uses: Eq.mpr, And, Eq, ArithmeticFunction, ArithmeticFunction.sigma, OfNat.ofNat, HAdd.hAdd, Ne, id, congrArg, propext, isAmicable_iff, Decidable.byContradiction, Not, Eq.mp
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem IsAmicable.symm {a b : ℕ} (h : IsAmicable a b) : IsAmicable b a := by
…
```
Mentions: IsAmicable
theorem AmicableNumbers.relatively_prime_amicable Relatively prime amicable numbers conjecture sorry line 66 source
Source documentation
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

L4DEL explanation
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
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, IsAmicable, Ne, Nat.Coprime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem relatively_prime_amicable :
    answer(sorry) ↔ ∃ a b : ℕ, IsAmicable a b ∧ a ≠ b ∧ a.Coprime b := by
…
```
Mentions: IsAmicable
theorem AmicableNumbers.infinitely_many_amicable Infinitely many amicable numbers conjecture sorry line 81 source
Source documentation
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

L4DEL explanation
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
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Prod, Nat, Set.ofPred, Erdos830.erdos_830.parts.i.match_1, IsAmicable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem infinitely_many_amicable : type_of% Erdos830.erdos_830.parts.i := by
…
```
Mentions: Erdos830.erdos_830.parts.i
theorem AmicableNumbers.opposite_parity_amicable Amicable numbers with opposite parity conjecture sorry line 94 source
Source documentation
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

L4DEL explanation
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
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, IsAmicable, Even, Odd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem opposite_parity_amicable :
    answer(sorry) ↔ ∃ a b : ℕ, IsAmicable a b ∧ (Even a ↔ Odd b) := by
…
```
Mentions: IsAmicable