Must a near-squaring integer sequence with rational reciprocal sum be Sylvester's sequence? (Erdős #243)
Statement
Let $1\le a_1<a_2<\cdots$ be a strictly increasing sequence of integers with $$\lim_{n\to\infty}\frac{a_n}{a_{n-1}^2}=1$$ and with rational reciprocal sum $\sum_{n}\frac{1}{a_n}\in\mathbb{Q}$. Prove that then $a_n = a_{n-1}^2 - a_{n-1} + 1$ for all sufficiently large $n$ — i.e. the sequence eventually coincides with Sylvester's sequence $2,3,7,43,1807,\ldots$ (each term one more than the product of all previous terms).
Acceptance. FULLY RESOLVES: prove the Erdős–Straus conjecture — every strictly increasing integer sequence with $a_n/a_{n-1}^2\to 1$ and $\sum 1/a_n\in\mathbb{Q}$ satisfies $a_n=a_{n-1}^2-a_{n-1}+1$ for all large $n$ — with a complete proof; a Lean/Coq formalisation is preferred, otherwise a full written proof with every step. ADVANCES (each checkable): prove the conjecture under a named hypothesis strictly weaker than Duverney's convergence assumption stated in the background, with a proof that specifies exactly which hypotheses are used; or prove a strengthened structural constraint that strictly improves on the Erdős–Straus $\limsup$ inequality stated in the background. Deliver the proof file (formal or fully written), delimiting exactly the hypotheses used.
Background
Conjectured by Erdős and Straus; stated in Erdős–Graham [ErGr80, p.64] and [Er88c, p.105]. Listed as open on erdosproblems.com/243 (fetched 2026-07-13, status 'open', tagged 'number theory | irrationality'); a Lean 4 formalisation exists in google-deepmind/formal-conjectures. Sylvester's sequence $a_n=a_{n-1}^2-a_{n-1}+1$ (OEIS A000058) satisfies $\sum 1/a_n = 1$ exactly and grows doubly-exponentially ($a_n\sim c^{2^n}$), so it lies exactly on the boundary $a_n/a_{n-1}^2\to 1$ and has rational sum; the conjecture asserts it is essentially the ONLY such sequence. Partial results: Erdős and Straus [ErSt64] proved that any boundary sequence with rational sum that does NOT satisfy the recurrence must have $\limsup_{n\to\infty}\frac{[a_1,\ldots,a_n]}{a_{n+1}}\big(\frac{a_n^2}{a_{n+1}}-1\big)>0$, where $[a_1,\ldots,a_n]$ denotes the least common multiple — a strong structural constraint. Duverney [Du01] proved a weakened form: if the stronger series $\sum_{n}\big(\frac{a_{n+1}}{a_n^2}-1\big)$ converges, then $\sum 1/a_n$ is rational if and only if the Sylvester recurrence holds for all large $n$. No Erdős prize is recorded. Attacker's tool: irrationality and transcendence machinery for fast-converging series (à la Erdős–Straus and Duverney — least-common-multiple growth estimates and continued-fraction / gap arguments), with a proof assistant such as Lean as the target for a fully verified argument; direct computation offers little purchase because the claim is universally quantified over all admissible sequences.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #243 (T. F. Bloom) | website |
| REF-02 | OEIS A000058 — Sylvester's sequence a(n+1)=a(n)^2-a(n)+1 | website |
| REF-03 | Lean 4 formalisation — google-deepmind/formal-conjectures #243 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.