{"id":"palomar/PALOMAR-2026-10-30-000010","url":"https://github.com/jasondavies/nair-tenenbaum-short-sums/tree/9c3c9236a66f9ba1e04a237089ff836adde0cd6c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000010-v1.json","repo":"https://github.com/jasondavies/nair-tenenbaum-short-sums","tags":["math.NT","msc:11N37","msc:11N36","msc:11N25","msc:11N32"],"score":0,"title":"Short sums of certain arithmetic functions (Nair–Tenenbaum)","trust":"high","domain":"math.NT","source":"palomar","authors":["Jason Davies"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization of Nair and Tenenbaum's uniform upper bounds for short sums of nonnegative arithmetic functions evaluated at integer polynomial values. Theorem 1 retains the coefficient-independent height threshold and the restricted-discriminant dependence of the bound. Theorem 2 gives a greatest-prime-factor bound with a strict exponential gain for arbitrary nonconstant irreducible integer polynomials, including those with fixed prime divisors. Theorem 3 treats prime arguments with the explicit constant-term correction. The development also proves the ten corollaries on…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"Short sums of certain arithmetic functions","identifier":"doi:10.1007/BF02392880","relationship":"formalizes"},{"title":"Sur une question d’Erdős et Schinzel, II","identifier":"Inventiones Mathematicae 99 (1990), 215–224","relationship":"adapts"}]}