{"id":"palomar/PALOMAR-2026-10-22-000026","url":"https://github.com/sthubbar/goldbach-lean/tree/4d87394fed5e86a866ec2335621dc1b57f2e0c9d/entries/bombierivinogradov1965","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000026-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11N13","msc:11N35","msc:11M20","analytic-number-theory","sieve-methods","lean-formalization","prime-distribution"],"score":0,"title":"The Bombieri-Vinogradov theorem, Bombieri 1965 and A. I. Vinogradov 1965, classical form with the maximum over y <= x","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A sorry-free Lean 4 proof of the Bombieri-Vinogradov theorem in its classical form: for every A > 0 there is B > 0 such that the sum over q <= x^{1/2} (log x)^{-B} of the maximum over y <= x and over reduced residues a mod q of |psi(y; q, a) - y/phi(q)| is << x (log x)^{-A}. The same form is proved for theta(y; q, a), for pi(y; q, a) against liD(y)/phi(q) with liD(y) the sum of 1/log n over 2 <= n <= y, and for pi(y; q, a) against pi(y)/phi(q), the level of distribution 1/2 input of sieve methods. The proof runs from a zero-free region for Dirichlet L-functions and Siegel's theorem through…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"On the large sieve","identifier":"doi:10.1112/S0025579300005313","relationship":"formalizes"},{"title":"The density hypothesis for Dirichlet L-series","identifier":"Izv. Akad. Nauk SSSR Ser. Mat. 29, 1965, 903-934","relationship":"formalizes"}]}