---

Kovač, Vjekoslav and Tao, Terence, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), 572–608 (arXiv 2406.17593, whose third version, posted 2024-11-27, first carries this theorem and first names Tao as coauthor; versions 1 and 2 were Kovač's single-author note on simultaneous rationality of two Ahmes series). Theorem 2.11 of the paper constructs a strictly increasing sequence of positive integers $a_n$ with $\sum 1/a_n$ convergent such that

$$\sum_{n}\frac{1}{a_n+t}$$

is rational for every rational $t$ other than the poles $t=-a_n$. In particular no integer $t\ge1$ makes the shifted sum irrational, so the statement of Problem 266, a conjecture of Stolarsky, is false. The construction enumerates the rationals, works in the triangular rational coordinates of the paper's Section 7, and lets the number of shifts handled at once grow through a diagonal approximation; it concerns one specially built sequence and says nothing about standard sequences such as $n!$. The source card carries the digest.

Acceptance. Refereed: Acta Mathematica Hungarica, volume 175 (2025). Reviewed: the erdosproblems.com page for Problem 266 (last edited 2025-09-28) is labeled disproved by the site's curator, Thomas Bloom, who credits Kovač and Tao with the negative answer and states the stronger all-rational-shifts result; the site lists no proof claim, and the problem's forum thread has no comments. The formal-conjectures statement file for the problem tags both the negation and the all-rationals variant research solved. This corpus has not reproved the theorem and awards no tier of its own.

Formalization. A public Lean 4 development in Boris Alexeev's lean-proofs repository declares itself a formalization of Kovač and Tao's solution, names them as the informal authors and lists Codex and GPT-5.6 Sol as its formal authors; its theorem not_erdos_266, at the linked line of the commit of 2026-09-15, states the negation of the problem's assertion for sequences of positive integers with summable reciprocals, and the file aliases it to the formal-conjectures name erdos_266, whose formal_proof attribute cites that line. The file entered the repository on 2026-08-16. The development specializes the paper's block construction to positive integer shifts, so it formalizes the disproof and not the all-rationals theorem. Not built or audited here: neither the development nor the agreement of its statement with the problem's formulation was checked in this repository, so the formalization is a link and not acceptance evidence.

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