Problem 967

../

claims/: The 1 claim page of Problem 967, one per claimant's result; the problem's standing derives from them.

---

Statement. 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?$$

Status. DISPROVED (LEAN). The site credits Yip [Yi25], whose representation theorem yields, for each real $t\neq 0$, an admissible infinite sequence with $1+\sum_k a_k^{-(1+it)}=0$; its Lean marker refers to a third-party formalization that this corpus has not built, and it records the finite-sequence variant as open. The standing derives from Yip's claim page.

Source. erdosproblems.com/967, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #967, https://www.erdosproblems.com/967.

References.

• [ErIn64] Erdős, P. and Ingham, A. E., Arithmetical Tauberian theorems. Acta Arith. (1964), 341-356.
• [Yi25] F. Yip, On a problem of Erdős and Ingham. arXiv:2512.16528 (2025).

Formalization. The formal-conjectures statement file states the exact infinite-sequence target with sorry bodies and points, through its formal_proof attribute, to a Lean proof generated by Aristotle from Yip's TeX source; that proof negates an arbitrary-set statement, and it and Boris Alexeev's re-hosting of it are formalization links on the claim page. The corpus has built none of these files; see the Current assessment.

Current assessment

The source statements are recorded in Yip’s source home and [[../library/analysis/erdos_1964_arithmetical_tauberian_theorems/_index|Erdős–Ingham’s source home]]. Yip's Theorem 1.3 and Lemma 2.1 are recorded with proof sketches on their result pages. The additional infinite-tail refinement and the exact E0967 transfer were separately authored and independently reviewed as part of the complete natural-language chain; see the filed [[../library/analysis/yip_2025_problem_erdos_ingham/evidence/verify/full_proof_review|full-proof review]] and [[../library/analysis/yip_2025_problem_erdos_ingham/evidence/verify/refinement_audit|refinement audit]]. The review records are kept under the source's [[../library/analysis/yip_2025_problem_erdos_ingham/evidence/verify/_index|verification records]]. Erdős--Ingham's external Tauberian proof is contextual here and is not reconstructed in the corpus.

The arXiv record, lists only v1 and no journal reference; this does not establish peer-review acceptance. The site's thread carries no further claim on the exact question: a comment of 18 July 2026, in which the poster credits the observation to Claude Opus, argues that Schanuel's conjecture would imply nonvanishing for every finite sequence, and a comment of December 2025 links a preprint that proposes a reformulation and research directions. Neither is a dated manuscript claiming this problem, so neither has a claim page.

The formal evidence has a separate limitation. In the formal-conjectures statement file, at the commit the link pins, erdos_967 and its yip variant state the exact StrictMono infinite-sequence target, but their bodies use sorry. The formal_proof annotation links a proof reported by Lawrence Wu using Aristotle. In the gist, at the revision the link pins, main_theorem provides an arbitrary set $S$ with the prescribed sum and reciprocal summability, without asserting infinitude. Its final disproof negates an arbitrary-set target. There are no literal sorry or admit tokens in the gist, but the source alone does not certify a successful build. The required infinitude and increasing-enumeration transfer to the exact infinite sequence target is missing from the gist. The header declares Lean 4.24.0 and pins a Mathlib commit; the corpus has built none of these files or checked their axioms. Thus the Lean qualifier is unverified, independently of the preprint result.

Primary sources: Yip v1 and Erdős–Ingham 1964.

Progress

Yip's On a problem of Erdős and Ingham, arXiv:2512.16528v1 (18 December 2025), Theorem 1.3 (printed/physical pp.1–2), states that for every real $t\ne0$ and every $\lambda\in\mathbb C$ there is $S\subseteq\mathbb Z_{\ge2}$ such that

$$\sum_{n\in S}\frac1n<\infty, \qquad \sum_{n\in S}\frac1{n^{1+it}}=\lambda.$$

The paragraph immediately after the theorem on p.2 explicitly allows $S$ to be infinite, contained in $\mathbb Z_{\ge N}$ for any prescribed positive integer $N$, and to satisfy $\sum_{n\in S}1/n\le |\lambda|+\delta$ for any $\delta>0$. Choose one fixed nonzero $t$ and $\lambda=-1$, require $S$ to be infinite, and enumerate it increasingly. Because $|n^{-(1+it)}|=1/n$, the complex series is absolutely convergent, so the increasing enumeration preserves its sum. This gives an admissible infinite integer sequence with

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

This specialization of the preprint theorem refutes the universal nonvanishing assertion. The statements of the underlying set representation are recorded, with sketches of the printed proof, in Lemma 2.1 and Theorem 1.3. The p. 2 sentence allowing $S$ to be infinite is asserted without a separate derivation in v1. Its omitted schedule is supplied in [[../library/analysis/yip_2025_problem_erdos_ingham/infinite_refinement|the infinite-tail refinement]], a separate project-authored completion from the same lemma. An adjustable cap and half-residual steps keep each residual nonzero, force infinitely many nonempty ordered blocks, and telescope to the claimed mass bound. A remote-singleton reduction proves the zero-target case as well. The supplement writes the exact increasing-enumeration transfer needed here. An independent strong mathematical and source review, retained as the [[../library/analysis/yip_2025_problem_erdos_ingham/evidence/verify/full_proof_review|full-proof review]], confirmed these source-derived details and the exact increasing-sequence transfer. Their separate authorship does not make them part of the printed v1 proof and gives no formal or peer-review-acceptance credit.

Yip's Conjecture 3.1 and Question 3.2 (p.3) retain the finite-set question and $S=\{2,3,5\}$ respectively. Their nonvanishing assertions are open in that source. The general infinite construction does not resolve these finite questions.

The historical locators are separate. Erdős and Ingham, Arithmetical Tauberian theorems, Acta Arith. 9 (1964), printed p.341 / physical p.1, begin with a finite or infinite nondecreasing sequence of real numbers $1<a_1\le a_2\le\cdots$ with finite reciprocal sum. Theorem 4 is on printed p.347 / physical p.7. It equates nonvanishing on $\operatorname{Re}s=1$ with the Tauberian implication for their class $\mathcal I$ of nonnegative, nondecreasing, locally bounded functions vanishing below $1$ (defined on p.342). The distinct-integer question and $\{2,3,5\}$ discussion are on printed p.355 / physical p.15; the authors call the latter a simple case, without claiming it is the simplest. The modern strictly increasing integer formulation is Yip's Question 1.1 on p.1.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_1964_arithmetical_tauberian_theorems
• yip_2025_problem_erdos_ingham
• yip_2025_problem_erdos_ingham / evidence/verify/full_proof_review
• yip_2025_problem_erdos_ingham / infinite_refinement
• yip_2025_problem_erdos_ingham / lemma_2_1
• yip_2025_problem_erdos_ingham / theorem_1_3