TaoFivePrimes.primorial_certificate_2999

Proved

by chstdu · 1 vote · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorymertens-theoremnumber-theory

Exact primorial certificate for the primes up to $2999$ :

\prod_{p \le 2999,\; p \text{ prime}} p = N \quad\text{and}\quad \prod_{p \le 2999,\; p \text{ prime}} (p-1) = D,

with $N$ and $D$ the two explicit integers stated in the formal statement (an $1274$ -digit primorial and its shifted product). This is a pure finite data certificate: it anchors the Rosser–Schoenfeld product-bound legs above $2000$ the same way the primorial certificates at $691$ , $1049$ and $1499$ anchor the legs below, so that each range leg only has to telescope the Euler product over its own primes instead of re-verifying the primorial from scratch.

Preamble

import Mathlib.NumberTheory.PrimeCounting

Formal statement


namespace TaoFivePrimes
theorem primorial_certificate_2999 :
    ∏ p ∈ Nat.primesLE 2999, (p : ℕ) = 32168045701294620640542784528790339948233877194320691942185145891299282267301827858653888571839060683272964561610584928186988417578628002164703214171886786674939229756995037948648764395815023828302075665575157444314888026597263860661329372914653569353793099298110675747350882790738560504203040701810341941708299622684490034096044813598620265415917639053746497235391136440302245789388254695779136731649800394506848929333145878530882213856197884249924547399964854198069822375137903081024076929384147929193137113526392755836579289549478579290452268939901979700471063927494017934966444321544366172821328331594633610382125706058876853547226087239883300617652283490533003594791263352959054462749797306249090980395611964267800503252038457335033313795602693077546698568637990958724330204623439796907591665382645834031069255935284471220807454228319296688920584085335472718329592051095415453044678394165684806378988279115886003157346770618086197177915711919073761067762851185521820721234741469743161977521133701014646127271467607781556452183022747304328968569762845560612547433674751786878599906965681440208752545256167893937149981302815649814189368936710313993410230722909653878077249333284817971697995680522014814159427306342163589001701963174986335625857360402348009648300874365370 ∧
    ∏ p ∈ Nat.primesLE 2999, ((p : ℕ) - 1) = 2250661787285002070702806521443040235104092031835415292794221597397584437804628204058397381722128402625201007878295594307089536103232254937864561358235086980753389231094810332539495218856674418832174796263994360508465802903099258931798562870534351504897572723611920885448531784517393915350568495577698064727684360657011106478336718356308670307659052557801544083096487419629172693030542078351409715279770264513113517096570119962680184090978795509159860790336384942386236709135002340097685877856524649789420696150827772363979869808324718871517247696272060750732303525355764650353689382069289218606706045434836207871979093758076334250770756042156458620770355626741784515731034351229691390081052021480440451809546271224325496426180757829251910972398482550717070957371511790153149212337974597390900705412499582249101147386646625828432303954360562509719933588351276063132544682692701119920516215293440523978193696102725361995688630130946904405714496463757383238617930083744952310790952389668882303502615957359659735164998763466571661688552043504555847464790803964957018808835122661158282968250467226394551991935673578232344148988548674229154351908126720000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 := by sorry
end TaoFivePrimes

Source

Pure finite computation certificate (companion to TaoFivePrimes.primorial_certificate_691, TaoFivePrimes.primorial_certificate_1049 and TaoFivePrimes.primorial_certificate_1499): the exact values of the primorial

\prod_{p\le 2999} p

and of

\prod_{p\le 2999}(p-1)

, to serve as the verified anchor for the range legs of Rosser–Schoenfeld Theorem 23 (4.10) above

2000

View graph