TaoFivePrimes.primorial_certificate_1499

Proved

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

analytic-number-theorymertens-theoremnumber-theory

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

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

with $N$ and $D$ the two explicit integers stated in the formal statement (a $636$ -digit primorial and its shifted product). This is a pure finite data certificate: it anchors the Rosser–Schoenfeld product-bound legs above $1500$ the same way primorial_certificate_1049 anchors the $1050\dots1500$ leg, 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_1499 :
    ∏ p ∈ Nat.primesLE 1499, (p : ℕ) = 100011775713705647342085876224360975961797385167350897112376838062839491706403647724797055114806863470526629265119013875729405872094348125336381177862315327337756031471587052331292418383036726372482033490351693487501409230172344128596112472095563271632363268545398961225854310999688208619313591547489806687667965084046501989049434026219938309572724551027466561881176834038780124568086124532342939117388224911695272555071630768591659766497862348377588582570253697963217670223561610427535259257647559986077636129283752115320063847932948216884266137873300503611682909412640192452523004992140524801473407384694287272469624328179700053211530 ∧
    ∏ p ∈ Nat.primesLE 1499, ((p : ℕ) - 1) = 7644458924765903939791595849932995460950911183143591071451064969902294374663663534628251872241110485794838588227767718580465803928825188965640307631439881015108813964130600182947159833788456481059763405517201298252250570846069965886057686295553351136066446499429203537142008098072781558941585792366409253844195747062671954583440637402477207835078289539506841545045273634662046899587214219963385515776705190792376687512566479130111998478277683291568245424002752359623738624237182451550514176362933187472842310732747396025541068149979007900816259053383552637861888000000000000000000000000000000000000000000000000000000000000000000000000 := by sorry
end TaoFivePrimes

Source

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

\prod_{p\le 1499} p

and of

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

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

1500

View graph