Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Odd-prime sum counting beyond exp260

Proved
OddGoldbach19.large_count_exp260

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

goldbachnumber-theorysieve-theory

Let r(s)r(s)r(s) count representations of sss by two odd primes, using the shared campaign definitions, and write R(n)=#{0≤s≤n:r(s)>0}R(n)=\#\{0\le s\le n:r(s)>0\}R(n)=#{0≤s≤n:r(s)>0}. For every natural number n≥e260n\ge e^{260}n≥e260,

R(n)≥1001799 n.R(n)\ge\frac{100}{1799}\,n.R(n)≥1799100​n.

This lowers the large-range threshold of the previously proved estimate from e410e^{410}e410 to e260e^{260}e260. It is a supporting counting estimate, not a complete19-prime campaign endpoint.

Preamble
import Mathlib
import Definitions.Def_Schnir_defs
Formal statement
theorem OddGoldbach19.large_count_exp260 (n : ℕ) (hn : Real.exp 260 ≤ (n : ℝ)) :
    (n : ℝ) * (100 / 1799) ≤ (((Finset.range (n + 1)).filter (fun s => 0 < Schnir.r s)).card : ℝ) := by sorry
Source
New explicit refinement of the existing Riesel-Vaughan interval-weighted argument, using the proved coefficient-five interval Goldbach estimate, proved .46 second-order prime counting, and shifted-square concavity. The cutoff260 is derived by the attached exact polynomial and tail comparisons, not quoted from the source paper. Context: Riesel and Vaughan, On sums of primes (1983).
Human review
  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Yuxuan Xu · Oct 31, 2026

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

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me