Conjectures.io

Number theory

Erdős 251

Is ∑n=1∞pn2n\sum_{n=1}^\infty \frac{p_n}{2^n} irrational? Here pnp_n is the nn-th prime (p1=2,p2=3,…p_1=2, p_2=3, \dots).

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ Irrational (∑' (n : ℕ), ↑(Nat.nth Nat.Prime n) / 2 ^ n)

What you must prove

import FormalConjectures.ErdosProblems.«251»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos251.erdos_251" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/251.lean

Source type SHA-256
sha256:8b8156a5bf7c346ce72c6bc3f71bd5cf3e84860f37b4ecfb41b959217ad82450
Task id
fc-379fc029-erdos251-erdos-251-e5f66aae3a-formalized-v1
Task commitment
sha256:d84fba18e008666052843729eaa4c6fc923c724b2f6a5a73c0c45fb4e96cb7b6

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.