Erdős Problem 696: Sequence Chains in Divisors

### What is the conjecture

Define $h(n)$ as the largest $\ell$ such that there exists a sequence of primes $p_1 < \cdots < p_\ell$ all dividing $n$ where $p_{i+1} \equiv 1 \pmod{p_i}$ for each $i$. Define $H(n)$ as the largest $u$ such that there exists a sequence of integers $d_1 < \cdots < d_u$ all dividing $n$ where $d_{i+1} \equiv 1 \pmod{d_i}$ for each $i$.

The open problems are:
1. Estimate the growth rates of $h(n)$ and $H(n)$ as $n \to \infty$.
2. Determine whether $H(n)/h(n) \to \infty$ for almost all $n$.

Erdős conjectured that the typical order of $h(n)$ is the iterated logarithm $\log^*(n)$.

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

**Sources:**
- https://www.erdosproblems.com/696

### Prerequisites needed

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

Building blocks (from Mathlib):
- Basic divisibility and modular arithmetic structures
- Prime factorization and divisor sequences
- Asymptotic analysis framework for arithmetic functions

Missing pieces:
- Formal definitions of $h(n)$ and $H(n)$ as maximum chain lengths under the specified congruence conditions
- Infrastructure for reasoning about "almost all" $n$ (density arguments in number theory)

Rating justification: The statement involves standard number-theoretic concepts (divisors, congruences, primes) that exist in Mathlib, but the specific chains $h(n)$ and $H(n)$ require custom definitions. The growth-rate questions are asymptotic in nature and would benefit from existing Mathlib asymptotic analysis, but require careful formalization of the "almost all" quantification in number theory.

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

* ams-11

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