A certified 1000-prime finite sieve weight bound

Proved

OAI.OddGoldbach23.finite_sieve_certificate

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

number-theory

There exists a set $Q$ of exactly $1000$ odd primes, all at most $7927$ , such that

\sum_{\substack{a,b\in Q\\b<a}} \prod_{\substack{p\mid a-b\\p>2\text{ prime}}}\frac{p-1}{p-2} \le 867861.

The product runs over distinct odd prime divisors of the positive difference $a-b$ . The outer sum counts each unordered pair of distinct elements of $Q$ once.

This finite bound controls the off-diagonal term in a second-moment estimate for sums of two odd primes. It is a reusable input toward refining the existing $25$ -prime Odd Goldbach formalization; this statement alone does not assert a new Goldbach bound.

Preamble

import Mathlib
open Finset

Formal statement

theorem OAI.OddGoldbach23.finite_sieve_certificate :
    ∃ Q : Finset ℕ, Q.card = 1000 ∧
    (∀ p ∈ Q, p.Prime ∧ p ≠ 2 ∧ p ≤ 7927) ∧
    (∑ a ∈ Q, ∑ b ∈ Q, if b < a then
      (∏ p ∈ (a-b).primeFactors, if 2 < p then ((p : ℝ)-1)/((p : ℝ)-2) else 1)
      else 0) ≤ (867861 : ℝ) := by sorry

Source

Finite certificate constructed on 2026-10-25 as a refinement of the existing 25-prime Schnirelmann–Mann formalization, https://prove2.me/theorems/ba75c64f-9452-4582-83b3-77b31da8e4dc . Mathematical method: Riesel–Vaughan (1983), On sums of primes, section 6. The 1000-prime parameter and exact computational bound are this contribution, not a quoted theorem of that paper.

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