---

Claim. The post of 27 February 2026 in the discussion thread of Problem 263, by Swarat Chaudhuri's account, reports that a DeepMind prover agent falsified the second question in Lean, fully autonomously from the formal-conjectures statement, and links the proof, the theorem erdos_263.parts.ii in the formal-conjectures file at the commit linked above, which the post says compiles with Lean 4.22. The erdosproblems.com wording then defined an irrationality sequence without requiring it to be increasing, and so did the formal statement. The informal summary the post gives, which it credits to Adam Zsolt Wagner: let $a_n=2^{3^n}$ except on a very sparse set of indices, where $a_n=2^n$; then $a_n^{1/n}$ has no limit, while standard arguments show that $\sum1/b_n$ is irrational for every sequence of positive integers $b_n$ with $b_n/a_n\to1$. Such a sequence is not increasing. The claimant is the organization, with the system named as the post gives it; authors lists the poster, whose real name the posting account carries, since the post prints no author's name.

Submission note. Posted to the erdosproblems.com forum by Swarat Chaudhuri on 27 February 2026:

Our DeepMind prover agent has falsified the second question in Lean. The proof was found fully autonomously; the only problem-specific human input was the formal problem statement, drawn from Formal Conjectures. The proof (compilable with Lean 4.22) is available here (theorem erdos_263.parts.ii).

Here's an informal summary of the proof (due to Adam Zsolt Wagner):

Let $a_n = 2^{3^n}$, except on a very sparse subset of indices where we set $a_n = 2^n$. For this sequence, the limit of $a_n ^ {1/n}$ does not exist, but standard arguments show that for every sequence $(b_n)$ as above, $\sum 1/b_n$ is irrational.

Looking at the proof and the problem more closely, we realized that Erdos’s original problem statement (https://renyi.hu/~p_erdos/1988-22.pdf; p.105) required $a_n$ to be increasing. Assuming you agree, it would be good to correct the statement. That said, the counterexample still seems somewhat interesting, so we thought we would share it with the community.

Covers. The second question only, in the wording without the hypothesis that the sequence be increasing. Nothing on the first question, whether $a_n=2^{2^n}$ is an irrationality sequence.

Why it is rejected. It answers a variant, not the Statement. The post answers the erdosproblems.com wording of the time, in which an irrationality sequence need not be increasing. As the post itself observes, Erdős's statement requires the sequence to be increasing, and erdosproblems.com added that hypothesis on 2 April 2026; Problem 263 states the corrected question. The counterexample is not increasing, so it is not an irrationality sequence in the problem's sense and says nothing about whether every increasing one has $a_n^{1/n}\to\infty$. Its mathematics therefore answers the variant and does not settle this problem; the value disproved is its answer to that variant.

Standing. Rejected, as answering a variant. The erdosproblems.com remarks credit DeepMind with the counterexample to the earlier wording, and the formal-conjectures file keeps a link to the proof at the commit before the correction; no review of the proof is recorded, and this corpus has neither built nor audited it, so it gives a formalization link and no formalized evidence.

Depends on. No page of this wiki.