Hailey Collet · HaileyCollet@gmail.com

The appeal of this manuscript is how compact the self-contained argument is for c = 4/33, giving a zero-free half-plane Re(s) > 29/33, with the usual pole exclusions. Shiva Kintali’s proof for c = 1/48 is what started me on this. His manuscript is 27 pages; this one is 36 pages for c = 4/33.

This is a single-compensating-prime alternative proof, with an independently usable unconditional moving-radical mixed moment. It is a non-record result: the 29/33 boundary is weaker than 7/8. The manuscript treats the Riemann zeta function, all Dirichlet characters of positive modulus, and finite-order Hecke characters over the Eisenstein field. Appendix D.3 supplies the unconditional mixed-moment theorem separately from the zero-free endpoint.

Lean formalization

I started the formalization to try out FrankenLean, then moved it to ordinary Lean, with substantial OpenAI Codex assistance and foundations from OpenAI/math.

The formalization has about 24,000 local Lean lines and 703 theorems, on top of about 478,000 lines of reused OpenAI source. Mathlib and Lean itself are additional dependencies.

The ordinary-Lean audit passed for all 1,087 local declarations. Lean, NanoDa and con-ron also accepted the exported proof closures for the four main statements: zeta, Dirichlet, Hecke, and the standalone Appendix D.3 estimate. These are local contributor checks; maintainer verification is still pending in QuasiRiemannTracker.

I developed the manuscript with assistance from OpenAI’s GPT-6 Pro. The notices credit the reused sources and retain their licenses.