Conjectures.io

Number theory

Erdős 15

Is it true that ∑n=1∞(−1)nnpn\sum_{n=1}^\infty(-1)^n\frac{n}{p_n} converges, where pnp_n is the sequence of primes? Note: In the problem statement, pnp_n is the nn-th prime, indexed such that p1=2,p2=3,…p_1=2, p_2=3, \ldots. We 0-index here to reflect how Nat.nth works.

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ Summable fun k => (-1) ^ (k + 1) * (↑k + 1) / ↑(Nat.nth Nat.Prime k)

What you must prove

import FormalConjectures.ErdosProblems.«15»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos15.erdos_15" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/15.lean

Source type SHA-256
sha256:fe6c809775c5e2a2fe8ac769e6b1da07de51b55d65e5aaf3fc8fa41d15a227ef
Task id
fc-379fc029-erdos15-erdos-15-771c332347-formalized-v1
Task commitment
sha256:758cf6ab9a3cea3df6f513ac09f61125ddad46ae450f441780fdc1b840ceb636

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.