certification

The Keiper–Li Ledger: λ₁, λ₂, λ₃ Certified in Lean 4

Li's criterion is the sharpest known equivalence between the Riemann hypothesis and a concrete sequence of real numbers. Define, over the nontrivial