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

Weil's criterion states that the Riemann Hypothesis holds if and only if W(f,f) ≥ 0 for every test function f in a suitable class, where W is a quadratic form attached to the nontrivial zeros of the Riemann zeta function. Since the supports of the test functions are unrestricted, this amounts to positivity for test functions supported in [−t, t], for every t > 0. For a single fixed t the statement is much weaker and has been proved for small t. We prove it for t = ½ log 5: 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. Every step of the proof, from the explicit formula to the last numerical inequality, is formalized in Lean 4 and checked by the Lean kernel. 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. Version 2 rewrites the opening of the abstract and of the Background section to state Weil's criterion precisely (all test functions, unrestricted supports) and to separate it from positivity on a single window; the theorems and proofs are unchanged from version 1. 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.