Catalan-Dickson Conjecture: Aliquot Sequence Boundedness

### What is the conjecture

For a positive integer $n$, define the **aliquot sequence** as the sequence $(s_0, s_1, s_2, \ldots)$ where $s_0 = n$ and $s_{i+1} = \sigma(s_i) - s_i$ for $i \geq 0$. Here $\sigma(m)$ denotes the sum of all positive divisors of $m$, and $\sigma(m) - m$ is the sum of proper divisors of $m$.

The **Catalan-Dickson conjecture** states that every aliquot sequence is bounded. Specifically, every such sequence either terminates (reaches 1), reaches a perfect number (a number equal to the sum of its proper divisors), or enters a cycle of sociable numbers (numbers that are part of a periodic cycle under the aliquot iteration, including amicable pairs as special cases of length 2).

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- - [Wikipedia: Aliquot sequence](https://en.wikipedia.org/wiki/Aliquot_sequence)
- [Wolfram MathWorld: Catalan's Aliquot Sequence Conjecture](https://mathworld.wolfram.com/CatalansAliquotSequenceConjecture.html)
- [ProofWiki: Catalan-Dickson Conjecture](https://proofwiki.org/wiki/Catalan-Dickson_Conjecture)
- [OEIS: Aliquot sequences](https://oeis.org/wiki/Aliquot_sequences)
- [Carl Pomerance: Aliquot Sequences](https://math.dartmouth.edu/~carlp/upintconf.pdf)

### Prerequisites needed

**Formalizability Rating:** 1/5 (0 is best) (as of 2026-02-09)

Building blocks (1-3; from search results):
- `Nat.divisors`, `Nat.sum_divisors` (Mathlib)
- `IsPerfect`, `properDivisors` (available or easily defined)

Missing pieces (exactly 2; unclear/absent from search results):
- `AliquotSequence` definition (recursive iteration under sum-of-proper-divisors)
- `IsEventuallyPeriodic` or `IsBounded` for the specific context of number sequences

Rating justification: Mathlib provides divisor operations and bounded/periodic sequence definitions. Only need to define the aliquot iteration function and formalize the three termination conditions. This is a straightforward setup that requires minimal new infrastructure.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-40

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)