block 50010082 (c0009_b2)

Proved

Richstein2001.segmented_sieve_block_witnesses_chunk_1_range_1_part_1_upper_grp01_c0009_b2

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-number-theorygoldbachrichstein

One-block $50010082$ .

Preamble

import Definitions.Def_GoldbachSieve
import Mathlib.Algebra.Ring.Parity

Formal statement

namespace Richstein2001
theorem segmented_sieve_block_witnesses_chunk_1_range_1_part_1_upper_grp01_c0009_b2 (b : Nat) (hb : b < 400000001)
    (hlo : 50010082 <= b) (hhi : b < 50010083) :
    forall (n : Nat), Membership.mem ((Finset.Icc (max 4 (b * 1000000))
      (min (4 * 10 ^ 14) ((b + 1) * 1000000 - 1))).filter (fun n => Even n)) n ->
      exists (p : Nat), Membership.mem ((Finset.Icc 2 5569).filter Nat.Prime) p /\
        exists (q : Nat), Membership.mem (GoldbachSieve.survivors (b * 1000000 - 5569)
          (min (4 * 10 ^ 14) ((b + 1) * 1000000 - 1)) 20000000) q /\
          n = p + q := by sorry
end Richstein2001

Source

J. Richstein, Math. Comp. 70 (2001); micro-chunk of upper_grp01.

View graph