---

Claim. W. Cook, Excluding the bounded negative part: Lean-checked rigidity for Erdős Problem #243, a note in the author's Plectis repository (the preprint link, pinned to the revision posted). Corollary 1.1 states: let $a_1<a_2<\cdots$ be positive integers with $a_{n+1}/a_n^2\to1$ and $\sum1/a_n\in\mathbb Q$, and put $P_n=\prod_{j<n}a_j$; if

$$\limsup_{n\to\infty}\frac{P_n}{a_n}\Bigl(\frac{a_n^2}{a_{n+1}}-1\Bigr)<+\infty,$$

then $a_{n+1}=a_n^2-a_n+1$ for all large $n$. The hypothesis bounds the weighted error from above only, where the Erdős--Straus condition on their claim page asks for a limit superior at most $0$ with the lcm in place of the product. The note derives the corollary from an integer-state theorem on the tail numerators $C_n$ of a rational sum: a bounded negative error caps the upward increments of $C_n$, and a Chinese-remainder block then excludes the forced crossings. Theorem 7.1 of the same note states that a sequence with $a_n^2/a_{n+1}=1+3/n+o(n^{-3})$ has an irrational reciprocal sum, so the problem's implication holds vacuously for such sequences. The note's footnote on authorship says that Cook built and directed the research infrastructure and reviewed the claims when Cook could, that AI agents did most of the research and drafting, and that Cook did not independently verify every claim; Cook's thread comment of 11 September 2026 says Astra wrote the note up and that it does not settle the problem. The note cites an author-posted preprint of I. O. Bado for a two-sided bounded-error theorem, recorded on the problem page.

Covers. The sequences of Problem 243 whose product-weighted error $(P_n/a_n)(a_n^2/a_{n+1}-1)$ is bounded above. Not covered: sequences whose weighted error is unbounded above, as the note says.

Standing. Claimed. The note is not refereed and not on arXiv, the thread records no check of it, and no proof claim was registered on the site's proof-claims tab. The formalization link is the repository's Lean file for the integer-state theorem; the transfer to Corollary 1.1 is an ordinary argument in the note's Section 4. This corpus has not built or audited that Lean, so it is a link and gives no formalized evidence.

Depends on. Nothing in this wiki.