FormalConjectures/Mathoverflow/434111.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

4 declarations, 2 contain sorry, 0 declared as axioms

Are prime numbers among sums of prime numbers distributed as $\frac n{2\ln(n)}$?

Reference:

mathoverflow.net/questions/434111

[Me18] Meštrović, R., Curious Conjectures on the Distribution of Primes Among the Sums of the First 2n Primes, arXiv:1804.04198 (2018), Conjecture 3.3.

Imports (1)
  1. def MathOverflow434111.S $S_n$ is the sum of the first n primes, i.e. $S_n=p_1+\dots+p_n$, $1$-indexed, matching the MathOverflow question line 40 source

    Source documentation

    $S_n$ is the sum of the first n primes, i.e. $S_n=p_1+\dots+p_n$, $1$-indexed, matching the MathOverflow question.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: Finset.sum, Finset.range, Nat.nth, Nat.Prime

    1 instances, coercions and auxiliary constants left out.

    noncomputable def S (n : ℕ) : ℕ := ∑ k ∈ Finset.range n, nth Nat.Prime k
  2. def MathOverflow434111.piRestricted Documented declaration: piRestricted line 45 source

    Source documentation

    $\pi_n$ counts how many of $S_1,S_2,\dots,S_n$ are themselves prime, i.e. $\pi_n$ as used on MathOverflow (compare to $\pi_n$ in [Me18, Conjecture 3.3], which instead ranges over $S_2,S_4,\dots,S_{2n}$).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: Finset.card, Finset.filter, Nat.Prime, MathOverflow434111.S, Finset.Icc, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    noncomputable def piRestricted (n : ℕ) : ℕ :=
…
  3. theorem MathOverflow434111.restricted_prime_number_theorem The conjecture claims that $\pi_n\sim\frac n{2\ln(n)}$ sorry line 60 source

    Source documentation

    The conjecture claims that $\pi_n\sim\frac n{2\ln(n)}$.

    In other words, primes are distributed among the much sparser sequence $(S_n)_n$ with essentially the same density as in the positive integers, up to a factor of $2$.

    MathOverflow 434111.

    [Me18] Meštrović, R., Curious Conjectures on the Distribution of Primes Among the Sums of the First 2n Primes, arXiv:1804.04198 (2018).

    L4DEL explanation

    The conjecture claims that $\pi_n\sim\frac n{2\ln(n)}$. In other words, primes are distributed among the much sparser sequence $(S_n)_n$ with essentially the same density as in the positive integers, up to a factor of $2$. MathOverflow 434111. [Me18] Meštrović, R., Curious Conjectures on the Distribution of Primes Among the Sums of the First 2n Primes, arXiv:1804.04198 (2018).

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Iff, True, Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, MathOverflow434111.piRestricted, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.log

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem restricted_prime_number_theorem :
    answer(sorry) ↔ ((fun n : ℕ => (piRestricted n : ℝ)) ~[atTop] (fun n : ℕ => (n : ℝ) / (2 * Real.log n))) := by
…

    Mentions: MathOverflow434111.piRestricted

  4. theorem MathOverflow434111.restricted_prime_number_theorem.variants.even_subsequence Meštrović's original formulation [Me18, Conjecture 3.3]: the sequence of sums of the first sorry line 69 source

    Source documentation

    Meštrović's original formulation [Me18, Conjecture 3.3]: the sequence of sums of the first $2m$ primes satisfies the Restricted Prime Number Theorem, $\pi(m, (S_{2m})) \sim \frac{m}{\ln m}$.

    depends on sorry what this means

    Statement uses: Iff, True, Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, Finset.card, Finset.filter, Nat.Prime, MathOverflow434111.S, HMul.hMul, OfNat.ofNat, Finset.Icc, HDiv.hDiv, Real.log

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

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem restricted_prime_number_theorem.variants.even_subsequence :
    answer(sorry) ↔
      ((fun m : ℕ => (((Finset.Icc 1 m).filter (fun k => Nat.Prime (S (2 * k)))).card : ℝ)) ~[atTop]
        (fun m : ℕ => (m : ℝ) / Real.log m)) := by
…

    Mentions: MathOverflow434111.S