---

Claim. The answer to Problem 1051 is yes: if $1\le a_1<a_2<\cdots$ are integers with $\liminf_{n\to\infty}a_n^{1/2^n}>1$, then $\sum_{n=1}^\infty 1/(a_na_{n+1})$ is irrational. This is Theorem 2 of the preprint of T. Feng, T. Trinh, G. Bingham and twenty-one coauthors, Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems, arXiv:2601.22401 (first version 2026-01-29, third version 2026-02-05), whose source card and digest record the statement. The paper classifies the problem as one of its two autonomous resolutions: a solution was first produced by the research agent Aletheia, built on Gemini Deep Think, during a December 2025 run over 700 open problems of the catalog, and the human authors wrote up the result. The claimants are the paper's authors; the system is named here as the paper names it. The paper's own account of the checking, in its third version: the December output was graded by five mathematicians, who split four to one over a single deduction, that standard comparison theorems for linear recurrences imply the needed estimate, and no agreement was reached even after internal debate; for this problem only, the paper therefore prints the output of a later model run made for ablation purposes, rewritten by the human authors with minor inaccuracies corrected as its Section 1.3 describes. Its Remark 2.2 reports that the raw output took strict inequalities in the proof of its Lemma 2 where only weak ones hold; the printed rewrite states them as weak inequalities, and the paper points also to Barreto's Lean 4 formalization.

Submission note. Posted to the site's forum by Kevin Barreto on 30 January 2026:

This preprint, by myself and collaborators, gives a positive answer to the stated question. The solution was found completely autonomously by an AI agent powered by Gemini Deep Think, but I will report on that in more detail in a few days, when the methodology is officially released by a Google DeepMind team. Also, I have formalised the solution to the original problem variant in Lean, which can be viewed here.

We are hoping to improve our results further, but this will take some time to explore.

(The site has been updated to address this comment.)

Formalization. The paper states that the solution was formalized in Lean 4 by Kevin Barreto, one of its authors. The formalization was posted on 2026-01-30 in the problem's forum thread (the formalization link) as a Lean web-editor state, not as a repository file, so no commit pins it and the thread is the posting of record; the post says it formalizes the solution of the original problem, not the stronger theorem of the companion paper. The catalog's statement file FormalConjectures/ErdosProblems/1051.lean (the record link, pinned at the commit of 2026-09-22 that moved the growth condition's lower limit into the extended reals) carries the category research solved and a formal_proof attribute pointing to that thread, while its own proof term is sorry. No build of the formalization, axiom printout or statement audit by this project is recorded, so the claim lists no formalized evidence; the Lean qualifier in the site's label PROVED (LEAN) rests on that formalization.

Acceptance. Reviewed: Thomas Bloom, the site's curator, labels the problem PROVED (LEAN) and credits the affirmative answer in the remarks to Aletheia, citing this paper (page last edited 2026-02-01); Bloom is not among the paper's authors. The community database records the problem as proved (Lean). The companion paper of Barreto, Kang, Kim, Kovač and Zhang, recorded at Barreto, Kang, Kim, Kovač and Zhang 2026, reproves the question as the $d=2$ case of a sharper theorem and credits the original solution to the agent. The arXiv record of the third version carries no journal reference and no DOI, so no refereed publication is listed, and no independent check of the proof by this project is recorded.

Depends on. No page of this wiki.