---

Fredy Yip, On a problem of Erdős and Ingham, arXiv:2512.16528v1 (18 December 2025), proves in Theorem 1.3 that for every real $t\neq 0$ and every $\lambda\in\mathbb C$ there is a set $S\subseteq\mathbb Z_{\ge 2}$ with $\sum_{n\in S}1/n<\infty$ and $\sum_{n\in S}n^{-(1+it)}=\lambda$, and states after the theorem that $S$ may be taken infinite. Fix one nonzero $t$, take $\lambda=-1$ and an infinite such $S$, and let $a_1<a_2<\cdots$ enumerate it. This is a sequence of integers greater than $1$ with finite reciprocal sum, and because $|n^{-(1+it)}|=1/n$ the series converges absolutely, so the enumeration keeps its sum:

$$1+\sum_k \frac{1}{a_k^{1+it}}=0.$$

The question therefore fails for infinite sequences. The construction says nothing about finite sequences, and the finite question, in particular for $\{2,3,5\}$, stays open (Yip's Conjecture 3.1 and Question 3.2).

Reviewed. The site's curator, Thomas Bloom, marks Problem 967 disproved and credits Yip's result in the site's commentary (last edited 20 December 2025). The arXiv record, lists one version and no journal reference, so the claim has no refereed evidence. The printed statements are recorded and their proof sketched, with its two local slips corrected, and the infinite-set remark, whose schedule the preprint does not write out, is completed on the source's library card; the corpus's own review, kept with the [[../library/analysis/yip_2025_problem_erdos_ingham/evidence/verify/_index|verification records]] there, awards no evidence kind.

Depends on. Yip's Theorem 1.3 and Lemma 2.1, as recorded and sketched in the library, and the [[../library/analysis/yip_2025_problem_erdos_ingham/infinite_refinement|infinite-tail refinement]] that completes the infinite-set remark.

Formalization. The Lean file that the formal-conjectures statement file points to is a proof generated by Aristotle from the preprint's TeX source and posted on 19 December 2025 (GitHub login llllvvuu) as a formalization of Yip's disproof. Its final theorem negates a statement about arbitrary sets of integers at least $2$, and the exact strictly increasing infinite-sequence target is stated in formal-conjectures with sorry. Boris Alexeev's lean-proofs repository re-hosts the gist's proof with a header naming Yip as informal author and Aristotle and Lawrence Wu as formal authors; its final theorem not_erdos_967 negates the same arbitrary-set statement. The corpus has built none of these files, so the claim lists no formalized evidence.