Weil positivity on a window of width log 5: a formal proof in Lean 4

Weil's criterion expresses the Riemann Hypothesis as the positivity of a quadratic form W attached to the nontrivial zeros of the Riemann zeta function. For test functions supported in a fixed window, positivity is an unconditional and much weaker statement. We give a proof, formalized in Lean 4 from the explicit formula to the last numerical inequality, that for every nonzero complex-valued C² function f supported in [−½ log 5, ½ log 5] the zero sum defining W(f,f) converges and Re W(f,f) > 0. The sum runs over all nontrivial zeros with multiplicity and does not assume that they lie on the critical line. On this window the prime powers 2, 3, and 4 enter the explicit formula. The proof rewrites Re W as a real-space quadratic form, bounds its infinite-dimensional part from below by comparison with a logarithmic kernel that is diagonal in the Legendre basis with harmonic-number eigenvalues, and reduces positivity, for each parity, to a 32×32 Schur complement and a bound on the projection residuals of 32 explicit functions. These finite conditions are verified with integer ball arithmetic evaluated by the Lean kernel, without native code; numerical tables generated outside Lean serve only as candidates and are recomputed and checked in the kernel, so no externally generated certificate is trusted. A separate Lean theorem gives a uniform lower bound c∫|f|² ≤ Re W(f,f) for all such f, with c > 0 independent of f and not evaluated numerically. Both formalizations depend only on the standard axioms, and the Lean FRO comparator, run by the author in an isolated environment with the standard Lean kernel and the independent NanoDa kernel, accepted each against a separately fixed statement. Recent computer-assisted work states positivity on comparable and larger windows, with finite certificates checked outside a proof assistant; our contribution is a proof in which every step is checked by the Lean kernel. The result does not address the Riemann Hypothesis. Lean development: https://github.com/moriryota/weil-positivity-log5-lean (release v1.0.0, doi:10.5281/zenodo.23031523). Generative AI systems were used extensively in this work; see the section "Use of generative AI" in the paper.