October 8, 2026· ~6 min readThe 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
July 15, 2026· ~22 min readLean 4 Formalization: Cayley Graphs, Peter-Weyl, and Hecke Operators This document reports on formalizing connections between finite Cayley graph spectral theory and modular forms in Lean 4. The session focused on inte