---

Claim. No strictly increasing sequence of positive integers $a_n$ with $a_1\ge2$, both $\sum1/a_n$ and $\sum1/(a_n-1)$ convergent with rational values, has $\limsup a_n^{1/2^n}>1$; that is, every sequence of the kind Problem 265 asks about satisfies $a_n^{1/2^n}\to1$, as Erdős believed. Kenta Kitamura posted the result in the problem's discussion thread on 2026-09-07 (the discussion link) as a Lean 4 formalization giving a negative answer to the question whether $\limsup a_n^{1/2^n}>1$ can be achieved, the question the site's commentary leaves open; the post discloses that the formalization was developed with assistance from ChatGPT and OpenAI Codex, using GPT-6 (Astra), and the repository's README names OpenAI Codex and ChatGPT Astra. The development is an independent proof with no informal author named, so it has its own page, with the human submitter as claimant.

Submission note. Posted to the site's forum by Kenta Kitamura on 7 September 2026:

I, Kenta Kitamura (KitaKen1 on GitHub), have prepared a Lean 4 formalization giving a negative answer to the following question listed on the Erdős Problems forum for Problem #265: $\limsup_{n\to\infty} a_n^{1/2^n}>1.$

GitHub: https://github.com/KitaKen1/erdos-265-lean Lean4Web: open the standalone proof

Verification: no 'sorry' or 'admit'; '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'.

AI Usage Disclosure: This formalization was developed with assistance from ChatGPT and OpenAI Codex, using GPT-6 (Astra).

The formal statement. The theorem erdos265_negative_answer of lean/Erdos265/Main.lean, at the repository's commit of 2026-09-07 (the first formalization link; the second is the standalone one-file version for Lean4Web at the same commit), negates the existence of a : ℕ → ℕ that is StrictMono, has 2 ≤ a 0, has both ∑' 1/(a n) and ∑' 1/((a n) - 1) summable over the reals and equal to rationals, and has some real c > 1 with c ^ (2 ^ n) ≤ a n for infinitely many n. The infinitely-often form is the README's robust formulation of $\limsup a_n^{1/2^n}>1$. The route is the stronger lemma erdos265_criticalBaseTwoConclusion, that $\log(a_n)/2^n\to0$ under the six hypotheses, proved through an eventual quadratic recurrence for a tail envelope and a second residual estimate that rules out a positive limit, as the README describes. The summability hypotheses are implicit in the problem's statement, which asks for rational values of the two sums, and $a_1\ge2$ is forced by the term $1/(a_1-1)$.

Covers. The growth question from above: $\limsup a_n^{1/2^n}>1$ is impossible, so the folklore bound $\lim a_n^{1/2^n}=\infty$, which already excludes faster growth through the first sum alone, is sharpened to $a_n^{1/2^n}\to1$ when both sums are rational. Not covered: the precise exponent, that is, the supremum of the bases $\beta$ with $a_n^{1/\beta^n}\to\infty$ possible, which lies between $\sqrt{6/5}$ (the accepted Kovač–Tao claim) or $(\sqrt{13}-1)/2$ (the pending Cam claim) and $2$.

Standing. Claimed. The post says that the files contain no sorry or admit and that #print axioms reports only propext, Classical.choice and Quot.sound; the README dates the modular proof to Lean 4.27.0 and the standalone file to Lean 4.34.0-rc2. The site labels the problem OPEN (page last edited 21 January 2026); as of 2026-10-07 the post has no replies, the curator has not commented on it, no write-up outside the repository exists, and the corpus records no build or audit of the development, so the claim lists no evidence.

Depends on. Nothing in this wiki.