Erdős problem 266

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.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

266.lean

Retained formal statement1 of 2

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).

FormalConjectures/ErdosProblems/266.leanErdos266.erdos_2662 linesExact file

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

SolvedStatement only, no proof