Prove2Me

θ\theta certificate, the base range, part 2

Proved
ThetaCert.base_p2

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theoryprime-numbers

The kernel checker accepts the listed certificate records (part 2 of ThetaCert.base, split to keep each kernel check within the time limit).

Preamble
import Definitions.Def_ThetaCertData_base
Formal statement
theorem ThetaCert.base_p2 :
    ∀ s ∈ [ThetaSieve.ThetaBase.s14, ThetaSieve.ThetaBase.s15, ThetaSieve.ThetaBase.s16, ThetaSieve.ThetaBase.s17, ThetaSieve.ThetaBase.s18, ThetaSieve.ThetaBase.s19, ThetaSieve.ThetaBase.s20], s.bok = true := by sorry
Source
P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442 (2010), Theorem 5.2 (k = 2, η = 0.2, x ≥ 3 594 641); here the range [3 594 641, 3 584 912 847] is closed by a kernel-checked sieve certificate.

View graph