PROVED LEANdatabase updated 2026-01-31
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The sequence \(u_1=1\), \(u_{n+1}=u_n(u_n+1)\), indexed here so that `u i` is \(u_{i+1}\): `u 0 = 1`, `u 1 = 2`, `u 2 = 6`, `u 3 = 42`, … (so `u i + 1` is Sylvester's sequence \(2, 3, 7, 43, \ldots\)).
The Vardi constant \(c_0=\lim u_n^{1/2^n}=1.264085\cdots\). With the `0`-indexing of `u`, the \(n\)-th term \(u_n^{1/2^n}\) of the defining sequence is `(u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))` at `i = n - 1`.
Let \(u_1=1\) and \(u_{n+1}=u_n(u_n+1)\), so that \(\sum_{k\geq 1}\frac{1}{u_k+1}\) and \(u_k=\lfloor c_0^{2^k}+1\rfloor\) for \(k\geq 1\), where \[c_0=\lim u_n^{1/2^n}=1.264085\cdots.\] Let \(a_1<a_2<\cdots \) be any other sequence with \(\sum \frac{1}{a_k}=1\). Is it true that \[\liminf a_n^{1/2^n}<c_0=1.264085\cdots?\] This is true, and was proved independently by Kamio [Ka25] and Li and Tang [LiTa25]. An earlier interpretation of this question on this site defined \(u_1=2\) and \(u_{n+1}=u_n^2-u_n+1\) (Sylvester's sequence), which is the same sequence shifted by \(1\); we use the phrasing above as more faithful to [ErGr80]. The constant \(c_0\) is called the Vardi constant.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/315.
NOBODY HAS SENT US AN ATTEMPT YET
If you take a run at this one — with your own AI subscription or without — the guide says how,
and the submission form gets you an honest read of what you found.