Reading OpenAI’s proof side by side with a Lean formalization
A quasi-Riemann Hypothesis in \(\Re(s)>11/12\)
We seek cancellation in Möbius over \(\mathbb Q\):
\(\displaystyle \sum_{n\asymp X}\mu(n)\)
It is well known that a power savings here is equivalent to quasi-RH.
But over \(\mathbb Q\) there are not enough
harmonics. We therefore lift to the Eisenstein field
\(K=\mathbb Q(\omega)\):
\(\displaystyle M(X):=\sum_{\substack{n\in\mathcal O\\\mathcal N(n)\asymp X}}\mu_K(n),\)
and aim to prove that \(M(X) \ll_\varepsilon X^{11/12+\varepsilon}\) for every \(\varepsilon>0\).
Since
\(\zeta_K(s)=\zeta(s)L(s,\chi_{-3})\), nonvanishing of
\(\zeta_K\) forces nonvanishing of both factors. We deform the
Eisenstein Möbius sum by sextic characters:
\(\displaystyle M_h(X):=\sum_{\substack{n\in\mathcal O\\ n\asymp X}}\mu_K(n)\chi_x(h)\)
and take a second moment:
\begin{equation}\label{eq:mean-square} S(X,H):=\sum_{\substack{h\in\mathcal O\\ h\asymp H}}|M_h(X)|^2 \end{equation}
We seek roughly square-root cancellation on average:
\(\displaystyle S(X,H)\ll XH,\)
ignoring epsilons.
By itself, that is not enough, because \(M(X)\) only appears once in \(S(X,H)\).
In the application, \(H=X^{1+\epsilon}\) will be a hair larger than \(X\), so even with square-root cancellation on average, dropping all but one term only shows the trivial bound: \(|M(X)|^2\le S(X,H)\ll X H \), which implies \(M(X)\ll (XH)^{1/2}\); this is epsilon worse than trivial - but in Sarnak's terminology, "pregnant". ("You have to be pregnant to deliver!")
But sixth powers act as an amplifier. They recover (almost) the
original sum:
\(\displaystyle |M_{p^6}(X)-M(X)|\ll XH^{-1/6}\quad\bigl(p\text{ prime},\ \mathcal N(p^6)\asymp H\bigr)\).
Since there are very roughly \(H^{1/6}\) (again, ignoring epsilons) such, we get, roughly, that
\(H^{1/6}|M(X)|^2\le S(X,H)\ll X H \), and hence \(M(X)\ll X^{1/2}H^{5/12}\), which gives the main result.
Opening the square in (1), first separate the diagonal \(n_1=n_2\): its contribution is \(O(HX)\), already of the required size.
To see the mechanism off the diagonal, ignore all but the other extreme, \((n_1,n_2)=1\).
Reversing orders and applying Poisson in \(h\) (write \(L=X^2/H\) for the dual length) gives schematically
\(\displaystyle S(X,H)\approx \frac1L\sum_{\ell\asymp L}\sum_{\substack{n_1,n_2\asymp X\\(n_1,n_2)=1}}\mu_K(n_1)\mu_K(n_2)\,\mathcal G_{n_1,n_2}(\ell),\)
where the unnormalized sextic Gauss factor has the shape
\(\displaystyle \mathcal G_{n_1,n_2}(\ell)=\sum_{a\bmod n_1 n_2}\overline{\chi_{n_2}(a)}\chi_{n_1}(a)\,e_K\!\left(\frac{\ell a}{n_1 n_2}\right).\)
The Gauss–Jacobi identity absorbs the Möbius signs into the Gauss factors on both sides, leaving cubic Gauss sums and explicit phase factors. Write the resulting normalized cubic-Gauss coefficient as
\(\displaystyle c_3(n):=\widetilde g_3(n)\,\overline{\frac{n}{|n|}}.\)
Here \(\widetilde g_3(n)\) is the cubic Gauss sum normalized by the square root of the norm, and \(n\) is the chosen primary generator. After rearranging the phases, the \(n_1\)- and \(n_2\)-sums recombine heuristically into an absolute square:
\(\displaystyle \begin{aligned} S(X,H)&\approx\frac{X}{L}\sum_{\ell\asymp L}\sum_{n_1,n_2\asymp X}\overline{\chi_{n_2}(\ell)c_3(n_2)}\,\chi_{n_1}(\ell)c_3(n_1)\\&=\frac{X}{L}\sum_{\ell\asymp L}\left|\sum_{n\asymp X}\chi_x(\ell)c_3(n)\right|^2.\end{aligned}\)
Coprimality restrictions and the remaining phase separation are suppressed in this schematic. Normalizing the two Gauss factors contributes a factor \(X\), changing the prefactor \(1/L\) to \(X/L=H/X\). We now recognize \(c_3(n)\) as the squarefree Fourier coefficients of Kubota’s cubic theta series.
For each fixed \(\ell\), restore the cube multiples \(mj^3\) to obtain the completed twisted theta coefficients, which we denote schematically by
\(\displaystyle \tau_\ell(n):=\sum_{\substack{mj^3=n\\m\ {\rm squarefree}}}\chi_m(\ell)c_3(m)\,w_\ell(j).\)
The cube weights \(w_\ell(j)\) include the required twists and normalizations. Completion replaces the inner squarefree sum by \(\sum_{n\asymp X}\tau_\ell(n)\); Möbius inversion in the cube factor recovers the original sum.
Thus the completed sums enter our second moment in the schematic form
\(\displaystyle S(X,H)\approx\frac{H}{X}\sum_{\ell\asymp L}\left|\sum_{n\asymp X}\tau_\ell(n)\right|^2,\)
with the cube-inversion sums and their scale changes left implicit.
The theta series is constructed as the residue of a metaplectic Eisenstein series, whose meromorphic continuation is obtained by Selberg’s resolvent/Fredholm method. Taking the residue preserves its automorphic transformation law, giving the theta series its modularity. This classical construction is an important component of the formalization.
Modularity of the completed theta series gives a Voronoi-type summation identity, whose main shape in this normalization is
\(\displaystyle \sum_{n\asymp X}\tau_\ell(n)\ \approx\ \frac{X}{L}\sum_{y\asymp Y}\tau^\vee_\ell(y),\qquad Y=\frac{L^2}{X},\quad \ell\asymp L.\)
Here \(\tau^\vee_\ell(y)\) denotes the normalized coefficients at the reflected cusps; the cusp sums and transformed smooth weights are implicit. The reflection kernel has scale \(X/\mathcal N(\ell)^2\), giving the dual norm length \(Y\). Substituting this transformation into the second moment gives
\(\displaystyle S(X,H)\approx\frac{H}{X}\frac{X^2}{L^2}\sum_{\ell\asymp L}\left|\sum_{y\asymp Y}\tau^\vee_\ell(y)\right|^2.\)
We then reopen the cube completion and separate the phases. The resulting quadratic energies have the schematic form
\(\displaystyle S(X,H)\ \approx\ \frac{H}{X}\frac{X^2}{L^2}\sum_{\ell\asymp L}^{*}\left|\sum_{y\asymp Y}^{*}a_y\,\overline{\chi_y(\ell)}^{\,3}\right|^2,\qquad Y=\frac{L^2}{X}.\)
The stars indicate admissible squarefree rows and columns; \(a_y\) are fixed coefficients within each block, with \(|a_y|\le1\). The sextic characters now occur cubed, so they are quadratic! The sharp quadratic large sieve gives, ignoring epsilon losses,
\(\displaystyle \sum_{\ell\asymp L}^{*}\left|\sum_{y\asymp Y}^{*}a_y\,\overline{\chi_y(\ell)}^{\,3}\right|^2\ll(L+Y)\sum_y^{*}|a_y|^2\ll(L+Y)Y.\)
Consequently, this heuristic gives
\(\displaystyle S(X,H)\ll\frac{HX}{L^2}(L+Y)Y=H(L+Y)\ll HX,\)
since \(1\le Y\le L\le X\) when \(H\) is just above \(X\). This explains the target bound. The full proof organizes the extra phases, common divisors, cube scales, and non-squarefree rows through a second Poisson passage and finite descent, obtaining \(S(X,H)\ll_\varepsilon XH\,X^\varepsilon\) in the required range. Sixth-power amplification then yields \(M(X)\ll_\varepsilon X^{11/12+\varepsilon}\).
Public endpoint11/12 < Re s → riemannZeta s ≠ 0
Proof objectsThe linked declarations compile; proof bodies remain in source