The P\'olya--Vinogradov inequality with $\log\log q$

Deep Bhattacharjee; Ushashi Bhattacharya

The P\'olya--Vinogradov inequality with $\log\log q$

A mix of human-written and AI-generated textHuman understanding: some partsmath.NT — Number Theory math.CA — Classical Analysis and ODEs

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 16, 2026 / CC BY 4.0

Abstract

We prove unconditionally that every primitive Dirichlet character

\chi

modulo

q\ge3

has character sums of size at most

C\sqrt q\log\log q

. Montgomery and Vaughan proved this bound under the generalised Riemann hypothesis, and Paley showed that it is optimal. The proof uses the zero-free half-plane

\Re s>7/8

, which also gives

|L'/L(1,\chi)|\ll\log\log q

and two-sided bounds for the Euler--Kronecker constants of the cyclotomic fields

\mathbb Q(\zeta_q)

.

Provenance statement

Deep Bhattacharjee chose the problem, set the requirements and reviewed the results. The proofs, the Lean 4 formalisation, the supporting computations and the text of the manuscript were developed with Claude (Anthropic), used through Claude Code. Theorems 1.1 and 1.3 and the exponential sum bound behind them are formalised in Lean 4 with Mathlib and checked by the Lean kernel. The formal proofs use only the standard axioms (propositional extensionality, choice and quotient soundness) and have no unproved steps. The one input not proved in the paper is the zero-free half-plane Re s > 7/8 for Dirichlet L-functions of nonprincipal characters. It comes from OpenAI's preprint "The quasi-Riemann hypothesis: a zero-free half-plane Re s > 7/8" (30 September 2026, https://github.com/openai/math), which has not been refereed. Its Lean proof was compiled from source and checked by the kernel together with ours, so the whole argument is machine-checked. The numerical steps of the proofs were also checked by independent programs in Python, Julia, C and C++, run by a shell script. The Lean files, the programs and the logs are archived at https://doi.org/10.5281/zenodo.23383716.

AI provenance filesAI_PROVENANCE_PolyaVinogradovLogLog.md · 3 KB

Tools used

Anthropic: Claude Code

References

Y. Ihara, V. K. Murty and M. Shimura, On the logarithmic derivatives of Dirichlet $L$ -functions at $s=1$ , Acta Arith. 137 (2009), 253--276, doi:10.4064/aa137-3-6 (https://doi.org/10.4064/aa137-3-6).DOI
H. L. Montgomery and R. C. Vaughan, Exponential sums with multiplicative coefficients , Invent. Math. 43 (1977), 69--82, doi:10.1007/BF01390204 (https://doi.org/10.1007/BF01390204).DOI
OpenAI, The quasi-Riemann hypothesis: a zero-free half-plane $\Re s>7/8$ , preprint, 30 September 2026, with a Lean 4 formalisation, https://github.com/openai/math.link

Version history

v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 15, 2026