---

Claim. Kovač, Vjekoslav and Tao, Terence, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), 572–608, on the card kovac_2024_several_irrationality_problems_ahmes_series. Theorem 2.5: if $(a_n)$ is a strictly increasing sequence of positive integers with $\sum_n 1/a_n<\infty$ and

$$\liminf_{n\to\infty} a_n^2\sum_{k>n}\frac{1}{a_k^2}>0,$$

then $(a_n)$ is not an irrationality sequence of this type, that is, there is a bounded sequence of integers $b_n$ with $b_n\ne0$ and $a_n+b_n\ne0$ for all $n$ such that $\sum_n 1/(a_n+b_n)$ is rational. The paper's definition includes the condition $b_n\ne0$, which its footnote 3 adds to the formulation of Erdős and Graham to make the question about $2^n$ meaningful. Corollary 2.6: a strictly increasing sequence of positive integers with $\limsup_n a_{n+1}/a_n<\infty$ is not an irrationality sequence of this type, which covers $a_n=2^n$. Section 5 makes the case $a_n=2^n$ explicit: the sums $\sum_n 1/(2^n+b_n)$ over all $(b_n)$ with values in $\{1,\dots,5\}$ fill a closed interval containing $3/4$, so some such $(b_n)$ gives $\sum_n 1/(2^n+b_n)=3/4$. The arXiv record 2406.17593 carries the paper from its third version, posted 2024-11-27, which first states Theorem 2.5 and Corollary 2.6 and first names Tao as coauthor; versions 1 and 2 are Kovač's single-author note On simultaneous rationality of two Ahmes series, whose second version (2024-07-10) already proves as its Theorem 2 that $2^n$, and every sequence with a uniform bound in place of the liminf condition, is not an irrationality sequence of this type.

Submission note. Posted to the site's forum by Vjekoslav Kovač on 17 December 2025:

I got Aristotle to formalize a negative answer to the first half of this problem. More precisely, I asked it to formalize the claim: There exists a sequence $(b_k)_{k=1}^{\infty}$ with values in the set $\{1,2,3,4,5\}$ such that the infinite sum $\sum_{k=1}^{\infty} \frac{1}{2^k+b_k}$ is a rational number.

First, I wrote up a LaTeX blueprint of the proof originally appearing in this paper. Aristotle took about 50 minutes to formalize it, producing a Lean file which compiles in under a minute. Then, I removed all links and comments from the Lean file and asked Gemini 3 Pro to literally translate the (now mysterious) main theorem back to English. Theorem translation reads correctly, so the Lean file seems to be proving the correct statement.

(I am new to Lean, so any comments or corrections are welcome.)

Formalization. Three public Lean 4 files declare themselves formalizations of this result, none built or audited in this corpus. Kovač's file of 2025-12-17 in Kovač's own repository (the first formalization link) states that Aristotle (Harmonic) auto-formalized Kovač's blueprint of the paper's proof and generated the rest of the file; its main_theorem proves that some $b_k\in\{1,\dots,5\}$ make $\sum_k 1/(2^k+b_k)$ rational, and Kovač announced it on the site's discussion thread the same day (the first discussion link). Boris Alexeev's lean-proofs file Erdos264b of 2025-12-18 (the second formalization link) adapts it to prove the formal-conjectures statement erdos_264.parts.i, the negation of the irrationality-sequence property for $2^n$, and cites the paper as the original human proof. The combined file of 2026-08-25 in the same repository (the third formalization link) merges it with the independent proof recorded on the Alexeev page and names Kovač and Tao as its informal authors.

Covers. The powers-of-two part: the answer is no, $a_n=2^n$ is not an irrationality sequence of this type. Not covered: the factorial part. For $a_n=n!$ the quantity $(n!)^2\sum_{k>n}(k!)^{-2}$ tends to $0$ and the ratios $a_{n+1}/a_n=n+1$ are unbounded, so neither Theorem 2.5 nor Corollary 2.6 applies; the paper's Theorem 2.7 gives only some irrationality sequence of this type asymptotic to $n!$, not a statement about $n!$ itself.

Acceptance. Refereed: Acta Math. Hungar. 175 (2025), 572–608. The site's commentary credits Kovač and Tao with the result but labels the problem OPEN, so that remark is not listed as reviewed evidence, and the Lean files give no formalized evidence. The corpus has not reproved the theorem and awards no tier of its own.

Depends on. Nothing in this wiki; the claim rests on the cited paper.