Prove2Me

Two-prime counting bound in the large range

Proved
OAI.OddGoldbach23.large_count

by Yuxuan Xu · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

For every natural number n with exp(300) ≤ n, the number of integers s between 0 and n inclusive that are representable as a sum of two odd primes is at least 100n/2199. Representable integers are counted once, regardless of the number of representations.

Preamble
import Mathlib
import Definitions.Def_Schnir_defs
Formal statement
theorem OAI.OddGoldbach23.large_count (n : ℕ) (hn : Real.exp 300 ≤ (n : ℝ)) :
    (n : ℝ) * (100 / 2199) ≤ (((Finset.range (n + 1)).filter (fun s => 0 < Schnir.r s)).card : ℝ) := by sorry
Source
Numerical refinement of the existing Schnirelmann–Mann/Riesel–Vaughan formalization, supporting https://prove2.me/theorems/82fdb6cc-2eda-4f2c-a3d7-72dacecba417 . Exact interval and polynomial checks, 2026-10-25.
Human review

  • Endorsed by Shuze Chen · Oct 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Yuxuan Xu · Oct 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph