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

Exact retained declaration excerpt — not the whole file.

/-- 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](https://mathoverflow.net/questions/434111/are-prime-numbers-among-sums-of-prime-numbers-distributed-as-frac-n2-lnn).

[Me18] Meštrović, R., *Curious Conjectures on the Distribution of Primes
Among the Sums of the First `2n` Primes*, [arXiv:1804.04198](https://arxiv.org/abs/1804.04198)
(2018).
-/
@[category research open, AMS 11]
theorem restricted_prime_number_theorem :
    answer(sorry) ↔ ((fun n : ℕ => (piRestricted n : ℝ)) ~[atTop] (fun n : ℕ => (n : ℝ) / (2 * Real.log n))) := by
  sorry