Skip to content

Erdős problem 967

Let 1<a1<⋯1<a_1<\cdots be a sequence of integers such that ∑1ai<∞\sum\frac{1}{a_i}<\infty. Is it true that, for every t∈Rt\in \mathbb{R}, 1+∑k1ak1+it≠0?1+\sum_{k}\frac{1}{a_k^{1+it}}\neq 0?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

967.lean

Retained formal statement5 of 5

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

FormalConjectures/ErdosProblems/967.leanErdos967.erdos_967.variants.yip2 linesExact file
∀ (t : ℝ),  t ≠ 0 → ∃ a, StrictMono a ∧ 1 < a 0 ∧ (Summable fun k => 1 / ↑(a k)) ∧ 1 + ∑' (k : ℕ), Erdos967.summand t (a k) = 0
SolvedStatement only, no proof