---

Claim. T. Alexander Lystad's proof claim of 1 August 2026 on the proof-claims tab of Problem 263 gives a Lean 4 and Mathlib proof of the folklore growth criterion that the erdosproblems.com remarks state: if a strictly increasing sequence of positive integers satisfies $c\,a_n^{2+\epsilon}\le a_{n+1}$ for all large $n$, for some $c,\epsilon>0$, then $\sum1/b_n$ is irrational for every sequence of positive integers $b_n$ with $b_n/a_n\to1$. The development, generated with Kimi K3 under Lystad's direction, is in the repository linked above, with the write-up PROOF.md; the entry says the build completes with no sorry outside the problem's first question, which it states as open.

Submission note. Posted to erdosproblems.com as a proof claim by T. Alexander Lystad (account alexander_lystad) on 1 August 2026, giving "Kimi K3" as the AI used:

A Lean 4 + Mathlib proof of the folklore growth criterion: if a strictly increasing sequence of positive integers satisfies c·a_n^{2+ε} ≤ a_{n+1} eventually for some ε, c > 0, then for EVERY sequence b_n with b_n/a_n → 1 the sum ∑ 1/b_n is irrational. Proof: if ∑ 1/b_n = p/q, then q·∏{n≤N} b_n · ∑{n>N} 1/b_n is a positive integer; forward iteration (a_{M+k} ≥ a_M^{2^k}) bounds the tail by C/a_N^{2+ε}, while backward iteration (a_{N-k} ≤ K·a_N^{θ^k}, θ = 1/(2+ε)) bounds the product by C^{N+1}·a_N^σ with σ = (2+ε)/(1+ε) < 2+ε — so the integer tends to 0, a contradiction. The criterion fails for a_n = 2^{2^n} by exactly an ε (there a_{n+1} = a_n²), so Q1 remains open. Notes: Verification: 'lake exe cache get && lake build' in the linked repository completes with zero 'sorry' outside the declared open obligation (Q1 is stated with an honest 'sorry'). Archived release: v1.0.0, DOI: <DOI from Zenodo>. The repository also contains a supporting zero-sorry package (including a formal proof that ∑ 1/2^{2^n} is irrational) and a fidelity-audited formal statement of the problem. Independently of this claim: the community formal statement in FormalConjectures (ErdosProblems/263.lean) omits the "increasing" hypothesis this site added on 2026-04-02, so its Q2 entry covers the pre-correction statement; reported upstream with fix PRs (google-deepmind/formal-conjectures issue #4677, PRs #4678 and #4679).

Why it is rejected. It does not address the Statement. Problem 263 asks whether $a_n=2^{2^n}$ is an irrationality sequence and whether every irrationality sequence has $a_n^{1/n}\to\infty$. The claim addresses instead the folklore sufficient criterion, a known result the erdosproblems.com remarks state, which $2^{2^n}$ misses by the $\epsilon$, as the entry says; it decides neither question, so its mathematics does not settle this problem. The value proved is its answer to the criterion.

Standing. Rejected, as not addressing the Statement. The entry carries four comments on erdosproblems.com and no review; this corpus has neither read the repository nor built the development, so it gives a formalization link and no formalized evidence.

Depends on. No page of this wiki.