proofmap

The Rankin–Selberg method for level-one cusp forms, formalised in Lean 4 with Mathlib: the simple pole of Σ|a(n)|²n⁻ˢ, L(f, 1+it) ≠ 0, a de la Vallée Poussin zero-free region and the explicit formula, each also stated for the discriminant Δ. Classical results, new formalisation. Unrefereed.

Three results in analytic number theory with interval-arithmetic certificates and a Lean 4 core: the log log Q in Wolke's prime-moduli large sieve is necessary; Λ is unbounded on a family sharing L(s,χ₋₇)'s functional equation; Λ > 0.23 for the Davenport–Heilbronn function. Unrefereed.