Problem Statement
Let $a_1<a_2<\cdots$ be a sequence of integers such that\[\lim_{n\to \infty}\frac{a_n}{a_{n-1}^2}=1\]and $\sum\frac{1}{a_n}\in \mathbb{Q}$. Then, for all sufficiently large $n\geq 1$,\[ a_n = a_{n-1}^2-a_{n-1}+1.\]
Categories:
Number Theory Irrationality
Progress
Erdős and Straus [ErSt64] proved that if $\lim a_n/a_{n-1}^2=1$ and $\sum \frac{1}{a_n}$ is rational, and $a_n$ does not satisfy the recurrence, then\[\limsup_{n\to \infty} \frac{[a_1,\ldots,a_n]}{a_{n+1}}\left(\frac{a_n^2}{a_{n+1}}-1\right)>0.\]A sequence satisfying the reucrrence $a_n = a_{n-1}^2-a_{n-1}+1$ is known as Sylvester's sequence.This problem has been formalised in Lean as part of the Google DeepMind Formal Conjectures project.
Source: erdosproblems.com/243 | Last verified: January 14, 2026