Erdős problem 967

Let $1<a_1<\cdots$ be a sequence of integers such that $\sum\frac{1}{a_i}<\infty$. Is it true that, for every $t\in \mathbb{R}$, $$1+\sum_{k}\frac{1}{a_k^{1+it}}\neq 0?$$

Yip [Yi25] has proved that this is not always true - in fact, for any real $t\neq 0$, there exists a sequence of integers $1<a_1<\cdots$ such that $\sum \frac{1}{a_i}<\infty$ and $1+\sum_{k}\frac{1}{a_k^{1+it}}=0$.

This was formalized in Lean by Wu using Aristotle.