Prove2Me

θ\theta certificate, the base range, part 0

Proved
ThetaCert.base_p0

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 0 of ThetaCert.base, split to keep each kernel check within the time limit).

Preamble
import Definitions.Def_ThetaCertData_base
Formal statement
theorem ThetaCert.base_p0 :
    ∀ s ∈ [ThetaSieve.ThetaBase.s0, ThetaSieve.ThetaBase.s1, ThetaSieve.ThetaBase.s2, ThetaSieve.ThetaBase.s3, ThetaSieve.ThetaBase.s4, ThetaSieve.ThetaBase.s5, ThetaSieve.ThetaBase.s6], 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