---

Claim. The answer to Problem 315 is yes, as the case $n=1$ of Kamio's Theorem 8 in the preprint Asymptotic analysis of infinite decompositions of a unit fraction into unit fractions: for a positive integer $n$ let $s_1(n)=n+1$ and $s_{i+1}(n)=s_i(n)^2-s_i(n)+1$, with $c_n=\lim s_i(n)^{2^{-i}}$; then every nondecreasing sequence $a_1\le a_2\le\cdots$ of positive integers with $\sum1/a_i=1/n$ and $a_i\ne s_i(n)$ for some $i$ has $\liminf a_i^{2^{-i}}<c_n$. For $n=1$ the excluded sequence $2,3,7,43,\ldots$ is Sylvester's and $c_1$ is the Vardi constant $1.264085\ldots$, so the theorem answers the site's question for all nondecreasing sequences, which include the strictly increasing ones the problem asks about. The proof (pp. 3--5) carries Soundararajan's comparison argument for finite representations over to infinite ones; the result page records it as read for structure only. Kamio's Problem 1 prints the Sylvester recursion defectively, which Theorem 8 does not depend on.

Acceptance. Reviewed: the site's curator, T. F. Bloom, marks the problem proved and credits Kamio and, independently, Li and Tang; the site was updated after a thread comment of 31 January 2026 reported that Kamio's paper had been formalized by the prover Aristotle from its arXiv source. Bloom is not an author of the paper. The paper is an author preprint, arXiv 2503.02317v1 (4 March 2025, the only version), with no journal record found on the arXiv listing or by a Crossref bibliographic query on 2026-09-18, so no refereed evidence is listed. The corpus has not verified the proof; the acceptance rests on the curator's credit. The problem's standing is also carried by the independent proof on Li and Tang's claim page, posted eleven days later; Li and Tang's Remark 1.13 records Kamio's proof as independent, and Kamio's preprint, the earlier of the two, does not cite theirs.

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 Theorem 8 itself, for monotone sequences and every $1/n$ with a $0$-based generalized Sylvester sequence, and it derives the problem's statement from it, 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, so no formalized evidence is listed.