TaoFivePrimes.primorial_certificate_2477

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 $2477$ :

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

with $N$ and $D$ the two explicit integers stated in the formal statement (an $1057$ -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_2477 :
    ∏ p ∈ Nat.primesLE 2477, (p : ℕ) = 7947796959600957702254862590703262317927824266262268612936395292533468766937017819269761787001554512094319330271761601621982822032279923629214580687104937613891355221964308065384715003733485767094408899660567910354378027852618672783912515042934115929598686696170785929860765172083423724317175919636895063846837689673347110139582101045906776752747713548888502637245278413236430803371939940944327500818539816966654608267773159311187380087419015738305436302023786598009719079254664035084898840569872138783363480874999098434419261979924138853793806772641876481686752611951606754623645192043606093612119866023100607121142421109996232705633558717209105804351125055876484295316416518651176796031957891656107576538096150126846040239117172235372515100358541946001063495018856487863347484450496713105861209334503481928981019296299312545913499683786460445436139059956771146553551112906298285358165029084018874067621716867111742336410370499909591635708002240346482779910294692571274141341088992904881261524386937824844664624867353709567182693015069127274152084293946370 ∧
    ∏ p ∈ Nat.primesLE 2477, ((p : ℕ) - 1) = 569011786562666949037620551340443056842126252433604037331985990037892940958188222990346005943446713359488723208382791291152267014343025085129344975289071335760417011241014357565210295834846765265058626743811934793524532980325089303614248192120788364383463681002076348735662897744811099521422585188167034402678300903316772899108484313267265954514858870931618242915007733789747425558073158941970040400841941648103022322873776940295321384956870417108790606889476191806307159188892060725243586205758711361916409751074220073190134102865712452617882651362372571861876575725780045117436206171382231973666695048489425882384368372969045366183503680701397965358099660902688465206676835638561314682256356292881790645334939952401253413990387305406332547665623562315964214868943789915174413768765344496704797284077689084025924173560724534815535455336132907101478663544743411279203706325057482759255581915463935500835754667113727505101297620152867638197039923200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 := 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 2477} p

and of

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

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

2000

View graph