TaoFivePrimes.primorial_certificate_1049

Proved

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

computational-number-theorymertens-theoremnumber-theoryprimorial

The product of all primes $p \le 1049$ — the primorial $1049\#$ — equals $24182018439667308311491694740494964858262843170756753910294272354409474727672198217498259086210186717774898099335412150587699250532501350980033878679944375270298065966946947573245949050135938086949538693769027535100486358307018027160166719764535702635258115355876461297644313137236946719127118231253130495039148528815868309161321137618000132092945812851475307003511732180156573679192888083405128921757809687016739335250549529382313019073090$ exactly, and the product of $p-1$ over the same primes equals $1942697914432968621660400651037724029997089476805766763319663641876534719441506925646293348459782987870236684125832138553844343576662203028376048118150841182089208991611529877497824116125806057253969321410021029495437258899370630954452339318655699968940271857959692515106600379132166582120941541163762954355192887278023095269072275537991352280761139555241687849362021663035397949653778432000000000000000000000000000000000000000000000000000$ .

These exact values extend the primorial certificate at $691$ to the anchor prime $1049$ , anchoring the finite verification of the Rosser–Schoenfeld Mertens-product bound (Theorem 23, inequality (4.10)) on the leg $1050 \le x \le 1500$ of the induction towards the five-primes theorem. The values are computed with a sieve of Eratosthenes and exact integer arithmetic.

Preamble

import Mathlib.NumberTheory.PrimeCounting

Formal statement

namespace TaoFivePrimes
theorem primorial_certificate_1049 :
    ∏ p ∈ Nat.primesLE 1049, (p : ℕ) = 24182018439667308311491694740494964858262843170756753910294272354409474727672198217498259086210186717774898099335412150587699250532501350980033878679944375270298065966946947573245949050135938086949538693769027535100486358307018027160166719764535702635258115355876461297644313137236946719127118231253130495039148528815868309161321137618000132092945812851475307003511732180156573679192888083405128921757809687016739335250549529382313019073090 ∧
    ∏ p ∈ Nat.primesLE 1049, ((p : ℕ) - 1) = 1942697914432968621660400651037724029997089476805766763319663641876534719441506925646293348459782987870236684125832138553844343576662203028376048118150841182089208991611529877497824116125806057253969321410021029495437258899370630954452339318655699968940271857959692515106600379132166582120941541163762954355192887278023095269072275537991352280761139555241687849362021663035397949653778432000000000000000000000000000000000000000000000000000 := by sorry
end TaoFivePrimes

Source

Exact integer computation (sieve of Eratosthenes, exact products). Downstream use: J.B. Rosser, L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), 64–94, §5, p. 73, Theorem 23 (4.10). Primorial reference: OEIS A002110. https://doi.org/10.1215/ijm/1255631807

View graph