FormalConjectures/ErdosProblems/15.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 15: Convergence of Series with Primes

Reference: erdosproblems.com/15

Imports (1)
  1. theorem Erdos15.erdos_15 Is it true that $\sum_{n=1}^\infty(-1)^n\frac{n}{p_n}$ converges, where $p_n$ is the sequence of primes? sorry line 44 source

    Source documentation

    Is it true that $\sum_{n=1}^\infty(-1)^n\frac{n}{p_n}$ converges, where $p_n$ is the sequence of primes?

    Note: In the problem statement, $p_n$ is the $n$-th prime, indexed such that $p_1=2, p_2=3, \ldots$. We 0-index here to reflect how Nat.nth works.

    Note: convergence here is convergence of the sequence of partial sums, which is what the problem asks about. Summable would be the wrong notion: it is unconditional summability, equivalent over $\mathbb{R}$ to absolute convergence, and $\sum_n n/p_n$ diverges.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, Filter.Tendsto, Nat, Finset.sum, Finset.range, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, OfNat.ofNat, HAdd.hAdd, Nat.nth, Nat.Prime, Filter.atTop, nhds

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_15 : answer(sorry) ↔
    ∃ l : ℝ, Tendsto (fun N => ∑ k ∈ Finset.range N,
      (-1 : ℝ) ^ (k + 1) * (k + 1) / (k.nth Nat.Prime)) atTop (𝓝 l) := by
…