{"id":"palomar/PALOMAR-2026-11-01-000029","url":"https://github.com/sthubbar/goldbach-lean/tree/da5cf9edad7896290771dfcab8feee2906399e3d/entries/chebyshev1852","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000029-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11N05","msc:11A41"],"score":0,"title":"Mémoire sur les nombres premiers","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof, with no unproved steps and no hypotheses, of explicit two-sided bounds for Chebyshev's function psi from P. L. Chebyshev, Mémoire sur les nombres premiers, 1852, with Chebyshev's constant A = log 2/2 + log 3/3 + log 5/5 - log 30/30 = 0.92129.... For every natural number n at least 30, psi of n is at least A n - 5 log n + 2 log 30 - 1; for every natural number n, psi of n is at most 6A/5 n + 2 log^2 n + 160. The proof uses Chebyshev's combination of log n!, log of the factorials of n/2, n/3 and n/5, and log of the factorial of n/30, as in the paper, with error terms weaker…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Mémoire sur les nombres premiers","identifier":"http://www.numdam.org/item/JMPA_1852_1_17__366_0/","relationship":"formalizes"}]}