Erdős Problem 266

Reference: erdosproblems.com/266

theorem Erdos266.erdos_266 (a : ℕ → ℕ) : ¬(((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun (x : ℕ) => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t)))

Let $a_n$ be an infinite sequence of positive integers such that $\sum \frac{1}{a_n}$ converges. There exists some integer $t \ge 1$ such that $\sum \frac{1}{a_n + t}$ is irrational.

This was disproven by Kovač and Tao in [KoTa24].

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem Erdos266.erdos_266.variants.all_rationals : ∃ (a : ℕ → ℕ), StrictMono a ∧ a 0 ≥ 1 ∧ ∀ (t : ℚ), (¬∃ (n : ℕ), t = -↑(a n)) → ∃ (q : ℚ), HasSum (fun (n : ℕ) => 1 / (↑(a n) + ↑t)) ↑q

In fact, Kovač and Tao proved in [KoTa24] that there exists a strictly increasing sequence $a_n$ of positive integers such that $\sum \frac{1}{a_n + t}$ converges to a rational number for all $t \in \mathbb{Q}$ such that $t \ne -a_n$ for any $n$.

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).