Prove2Me

θ\theta certificate, the base range, part 1

Proved
ThetaCert.base_p1

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

Preamble
import Definitions.Def_ThetaCertData_base
Formal statement
theorem ThetaCert.base_p1 :
    ∀ s ∈ [ThetaSieve.ThetaBase.s7, ThetaSieve.ThetaBase.s8, ThetaSieve.ThetaBase.s9, ThetaSieve.ThetaBase.s10, ThetaSieve.ThetaBase.s11, ThetaSieve.ThetaBase.s12, ThetaSieve.ThetaBase.s13], 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