Schnirelmann density $\sigma(A)\ge 1/35000$

Proved

Schnir.density_A

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

number-theoryschnirelmann-densitysieve-theory

Let $B=\{(p-3)/2 : p \text{ an odd prime}\}$ and $A=B+B$ . The Schnirelmann density

\sigma(A)=\inf_{N\ge 1}\frac{|A\cap\{1,\dots,N\}|}{N}

satisfies

\sigma(A) \;\ge\; \frac{1}{35\,000}.

This bound holds for every $N$ , with no "sufficiently large" condition, and it is what the additive argument iterates.

Formalization Note $\sigma$ is Mathlib's schnirelmannDensity, with classical decidability. $A$ is Schnir.A.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

open Classical in
theorem density_A : (1 : ℝ) / 35000 ≤ schnirelmannDensity A := by sorry

end Schnir

Source

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

Schnirelmann density σ(A)≥1/35000\sigma(A)\ge 1/35000σ(A)≥1/35000