---

Claim. The answer to Problem 315 is yes. Li and Tang's Corollary 1.7 in their paper On a conjecture of Erdős and Graham about the Sylvester's sequence proves their Conjecture 1.3: with Sylvester's sequence $u_1=2$, $u_{n+1}=u_n^2-u_n+1$ and $c_0=\lim u_n^{1/2^n}=1.264085\ldots$ (the Vardi constant), every other strictly increasing sequence $a_1<a_2<\cdots$ of positive integers with $\sum1/a_n=1$ has $\liminf a_n^{1/2^n}<c_0$. This is the site's question with the excluded sequence written directly; the site's own setup defines $u_1=1$, $u_{n+1}=u_n(u_n+1)$ and excludes $u_k+1$, which is the same sequence, and the constant is the same limit. The proof (p. 19 of the preprint) chains two theorems of the paper: Theorem 1.6 constructs, for any competitor $(a_n)$, an eventually Sylvester sequence $(c_n)$ of positive reals, with $c_{n+1}=c_n^2-c_n+1$ from some index $N\ge2$ on, such that $\sum1/c_n=1$, $\sum_{i<N}1/c_i<\sum_{i<N}1/u_i$ and $\liminf a_n^{1/2^n}\le\lim c_n^{1/2^n}$. Theorem 1.5 shows $\lim c_n^{1/2^n}<c_0$ for every eventually Sylvester sequence of positive reals that has the recurrence from some $N\ge2$ on, reciprocal sum $1$ and $\sum_{i<N}1/c_i<\sum_{i<N}1/u_i$. The paper's second route, Theorem 1.9, generalizes the statement to rationals conditionally on the eventually-greedy claim of Erdős and Graham; it is not needed for this problem, and it is the route the authors' journal paper publishes (see Acceptance).

Acceptance. Reviewed: the site's curator, T. F. Bloom, marks the problem proved and credits Li and Tang together with Kamio as independent proofs; Bloom is not an author of either paper. No refereed publication of Corollary 1.7 is recorded. The arXiv listing gives as journal reference the authors' paper Generalizing a conjecture of Erdős and Graham via best Egyptian underapproximations, Acta Mathematica Hungarica 177 (2025), no. 1, 41--63 (published online 13 October 2025; DOI 10.1007/s10474-025-01566-8), which is not held. Its published abstract says that the conjecture was recently resolved constructively by Kamio and independently by the authors and that the paper proves a generalization assuming the unproven eventually-greedy claim (its Theorem 1.6, the preprint's Theorem 1.9); its reference list cites arXiv:2503.12277 as a separate item; and Kovač and Tang cite the preprint for the proof of this problem and the journal paper only for the conditional theorem. So the journal paper is recorded as the publication of the conditional route, not of this claim. The result page records the corollary as read clause by clause with the proofs of Theorems 1.5 and 1.6 unread; the corpus has not verified the proof, and the acceptance rests on the curator's credit.

Independence. Kamio's preprint, which proves the statement for nondecreasing sequences and for every unit fraction in place of $1$, was posted eleven days earlier and has its own page, Kamio's claim page. Li and Tang's Remark 1.13 records Kamio's proof as independent and almost simultaneous; Kamio's preprint, the earlier of the two, does not cite theirs. Kovač and Tang's 2026 preprint re-derives the statement non-constructively from the conditional theorem of the journal paper (Kovač and Tang's claim page).

Formalization. The file Erdos315.lean in Boris Alexeev's lean-proofs repository at the pinned commit names Kamio, Li and Tang as the informal authors and the prover Aristotle and Alexeev as the formal authors; its main theorem is Kamio's general statement for monotone sequences and every $1/n$, from which it derives the case of this problem, recording in a comment that #print axioms reports only propext, Classical.choice and Quot.sound. It is linked above as a formalization of this result. The corpus has not built or audited it, and whether its constant matches the formal-conjectures statement's clause by clause was not checked, so no formalized evidence is listed; the formal-conjectures statement file for the problem is a sorry pointing at that file and is not linked here.