# AI provenance: The Pólya–Vinogradov inequality with log log q

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X)
and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914).

- Paper: https://github.com/creelie/Breakthrough-problems-3/blob/main/preprintPolyaVinogradovLogLog/PolyaVinogradovLogLog.pdf
- Lean formalisation and code: doi:10.5281/zenodo.23383716 (release v1.0.0; all versions doi:10.5281/zenodo.23383715)
- Repository: https://github.com/creelie/Breakthrough-problems-3

## Results

1. **Theorem 1.1.** For every primitive character χ modulo q ≥ 3 and every x ≥ 1,
   |∑_{n ≤ x} χ(n)| ≤ C √q log log q, with an absolute constant C.
2. **Theorem 1.3.** |L'/L(1, χ)| ≤ C log log q for nonprincipal χ, and
   −C log q log log q ≤ γ_q ≤ C log q for the Euler–Kronecker constant of
   Q(ζ_q), for every prime q ≥ 3.
3. **A weak form of the Montgomery–Vaughan bound.** This bound for exponential
   sums with multiplicative coefficients is used on the minor arcs.

## Who did what

- **Deep Bhattacharjee** chose the problem, directed the work, set the format
  and the target journal, and ran the computations.
- **Claude (Anthropic), used through Claude Code under his direction,**
  produced the following:
  - the proofs;
  - the Lean 4 formalisation (about 10,000 lines in `lean/Vinogradov/`);
  - the checking programs in Python, Julia, C and C++;
  - the figures;
  - the LaTeX text of the paper.
- No other AI system wrote any part of the paper or of the Lean proof of the
  results above.

## Input from other work

The proof uses one result that it does not prove itself. This is the
zero-free half-plane Re s > 7/8 for Dirichlet L-functions of nonprincipal
characters (Theorem 1.2 of the paper).

- **Source.** OpenAI proved it and formalised it in Lean 4 in "The
  quasi-Riemann hypothesis: a zero-free half-plane Re s > 7/8", 30 September
  2026, https://github.com/openai/math.
- **Status.** That preprint has not been refereed. The paper credits it as
  OpenAI's result.
- **How it is used.** Its Lean sources are included unchanged (Apache 2.0),
  together with the files they import from PrimeNumberTheoremAnd and
  rellich-kondrachov. They are compiled from source and checked by the Lean
  kernel together with our proofs. `NOTICE` gives the exact commits.

## How the results are checked

- **Lean 4.** Lean 4.34.1 with Mathlib v4.34.1. The main theorems are:
  - `Vinogradov.PV.polya_vinogradov_loglog` (Theorem 1.1);
  - `Vinogradov.logDeriv_one_le` and `Vinogradov.sum_logDeriv_one`
    (Theorem 1.3);
  - `Vinogradov.MV.weak_mv`.

  These theorems, OpenAI's half-plane theorem and every intermediate step
  listed in `lean/Axioms.lean` depend only on the standard axioms propext,
  Classical.choice and Quot.sound. There is no `sorry` and no added axiom.
- **Independent programs.** Four programs (`checks/check.py`, `check.jl`,
  `check.c`, `check.cpp`) check the numerical steps of the proofs. They
  include the Euler–Kronecker formula, tested against values computed from the
  Hurwitz zeta function for every prime q ≤ 1000.
- **Reproducing the checks.** `run_all.sh` runs the programs, the Lean build
  and the axiom check.

## What is not claimed

The Lean library also proves some consequences of the half-plane that other
people obtained first, among them a bound for the least prime primitive root
and a Lindelöf-type bound. These are not claimed as new and are not in the
paper.