Sums of two odd primes have positive density: $R(x)\ge x/69660$

Proved

Schnir.R_lower

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryschnirelmann-densitysieve-theory

Let $R(x)=\#\{0\le s\le x : r(s)>0\}$ be the number of integers up to $x$ that are sums of two odd primes. For every real $x\ge e^{2000}$ ,

R(x) \;\ge\; \frac{x}{69\,660}.

This follows from the first and second moments by Cauchy–Schwarz, with $69\,660=9^2\cdot 860$ .

Formalization Note The count is over integers $0\le s\le\lfloor x\rfloor$ .

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

theorem R_lower (x : ℝ) (hx : Real.exp 2000 ≤ x) :
    x / 69660 ≤ (((Finset.range (⌊x⌋₊ + 1)).filter (fun s => 0 < r s)).card : ℝ) := by sorry

end Schnir

Source

An explicit elementary constant for sums of primes (unpublished note, September 2026), eq. (15), §4

View graph

Sums of two odd primes have positive density: R(x)≥x/69660R(x)\ge x/69660R(x)≥x/69660

Sums of two odd primes have positive density: $R(x)\ge x/69660$