Prove2Me

TaoFivePrimes.primorial_certificate_1999

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 19991999:

∏p≤1999,  p primep=Nand∏p≤1999,  p prime(p−1)=D,\prod_{p \le 1999,\; p \text{ prime}} p = N \quad\text{and}\quad \prod_{p \le 1999,\; p \text{ prime}} (p-1) = D,

with NN and DD the two explicit integers stated in the formal statement (an 843843-digit primorial and its shifted product). This is a pure finite data certificate: it anchors the Rosser–Schoenfeld product-bound legs above 20002000 the same way the primorial certificates at 691691, 10491049 and 14991499 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_1999 :
    ∏ p ∈ Nat.primesLE 1999, (p : ℕ) = 289374641962945601852615669686352438557198389101635505921978687533534603184099103356713220245045689382193979028466556623300928386426868641265517885761774500699854169800840685305650571905326393891147443503522793860584071591452879655775734323993447280229950516208168456242859704539545043029470723016883062129865188983307445759944131787563777752236534042838736571825768147309875879568648761848492474692269075737993820510968847059797750137738579680583507041487685017149524627916063644375086068999495298981349776540320796738483271972712449573928869390146878678278551706732964746955815021418849063826580384371871911662113251288424597019051505811657455462629184223235168202635751562718522606516698622396025118884934399326179006093117580004591816199377853876305166538715269486496913965338299018641563718412655206993166415109405802877992948356769154670 ∧
    ∏ p ∈ Nat.primesLE 1999, ((p : ℕ) - 1) = 21318695391788852308325543179515634116436965804087601692605437679997516940709606444494450596622797877651376505188454084353589022894231532355415624909779533891535488703149965932739780360587935630157155128061386285262335861267200286496752751594394066174865873883126372165970775993185074498179053573683411043384723684322784419964904655113301313930041048193372902996964934432197524272756628130272632031362376908848375526368110926231304727588081267105377827513487850869288715972526051620749957426108847374643022261026806571293386443099126534975734731443456110139090800942624207468845683108311322265064438638240602085040444240990899422353063487984775929566707122727501372007615660762005355006980273528990976398399486332725213219624485086565945594673669079040000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 := 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 ∏p≤1999p\prod_{p\le 1999} p and of ∏p≤1999(p−1)\prod_{p\le 1999}(p-1), to serve as the verified anchor for the range legs of Rosser–Schoenfeld Theorem 23 (4.10) above 20002000.

View graph