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.