---

Claim. The answer to the second question of Problem 263 is no: there is a strictly increasing sequence of positive integers $a_n$ such that $\sum 1/b_n$ is irrational for every sequence of positive integers $b_n$ with $b_n/a_n\to1$, and yet $a_n^{1/n}$ does not tend to infinity, since $\liminf a_n^{1/n}=1$. Liam Price posted the result in the problem's discussion thread on 2026-05-09 (the discussion link), writing that GPT-5.5 Pro disproves the second question; the human submitter is the claimant here and the system is named as the post names it. The write-up, The Growth Question in Erdős Problem #263 (May 2026), is the preprint link. The post also carries a standalone Lean 4 file, auto-formalized with Aristotle and cleaned up with Claude Opus 4.7 in the post's words, whose theorem erdos263_growth_negative_answer states the displayed claim; the file travels inside the address of the post's live.lean-lang.org link, which encodes the whole file, and has no separate hosting, so the post is its link.

Submission note. Posted to the site's forum by Liam Price on 9 May 2026:

GPT-5.5 Pro disproves the second question here. The argument has been auto-formalised in Lean with Aristotle and cleaned up with Claude Opus 4.7.

Construction. The sequence is the concatenation of blocks of consecutive integers $[M_k,M_k+L_k)$ with $L_k=\max(1,\lceil k\log_2M_k\rceil)$ and $M_k$ chosen recursively so large that the blocks are far apart. Long blocks of consecutive integers keep $\liminf a_n^{1/n}=1$, while the gaps between blocks make the tail of $\sum1/b_n$ beyond any block, multiplied by a denominator of the partial sum, smaller than one and positive, so no rational value is possible; the post by Nat Sothanaphan of the same day explains that the two requirements, $L_k/\log M_k\to\infty$ and $L_k/M_k$ small, are compatible once $M_k$ grows fast enough, crediting GPT-5.5 Thinking for the discussion.

Covers. The second question: an irrationality sequence of the problem's kind need not satisfy $a_n^{1/n}\to\infty$. The first question, whether $a_n=2^{2^n}$ is such a sequence, is not touched.

Standing. Claimed. Nat Sothanaphan replied in the thread on 2026-05-09 that a standard check found no issues and that the Lean matched the paper, giving a ChatGPT conversation as the check's record; that is a forum remark, not acceptance. The site labels the problem OPEN (page last edited 2026-04-02), and the formal-conjectures catalog's file for the problem at its commit of 2026-09-18 (the record link) tags the second question, erdos_263.parts.ii, research open for the corrected statement, noting that a DeepMind proof for the statement without the increasing hypothesis is preserved at an earlier commit. No refereed or arXiv version is recorded, and the corpus records no build or audit of the Lean file so the claim lists no evidence.

Depends on. Nothing in this wiki.