TaoFivePrimes.primorial_certificate_691

Proved

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

computational-number-theorymertens-theoremnumber-theoryprimorial

The product of all primes $p \le 691$ — the primorial $691\#$ — equals $27771430913146044712156219115012732149015337058745243774375474371978395728107173008782747458575903820497344261101333156469136833289328084229401057505005215261077328417649807720533310592783171487952296983742789708502518237023426083874832018749447215424764928016413509553872836856095214672430$ exactly, and the product of $p-1$ over the same primes equals $2366660927422546456508646376195476887659583197882331786950929753142350492341792778933410457673892508547598023824969782634570171819986369738021902408498548219345392147187349931391317424140722450778304869023782402228638927984071853108228740053081041928192000000000000000000000000000000000000$ .

These exact values serve as the anchoring certificate for finite verifications of the Rosser–Schoenfeld Mertens-product bound (Theorem 23, inequality (4.10)) on the interval $700 \le x \le 1500$ , the next range leg above the accepted certificate range $286 \le x < 700$ used in the chain 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_691 :
    ∏ p ∈ Nat.primesLE 691, (p : ℕ) = 27771430913146044712156219115012732149015337058745243774375474371978395728107173008782747458575903820497344261101333156469136833289328084229401057505005215261077328417649807720533310592783171487952296983742789708502518237023426083874832018749447215424764928016413509553872836856095214672430 ∧
    ∏ p ∈ Nat.primesLE 691, ((p : ℕ) - 1) = 2366660927422546456508646376195476887659583197882331786950929753142350492341792778933410457673892508547598023824969782634570171819986369738021902408498548219345392147187349931391317424140722450778304869023782402228638927984071853108228740053081041928192000000000000000000000000000000000000 := 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