{"id":"palomar/PALOMAR-2026-10-22-000021","url":"https://github.com/jasondavies/iwaniec-linear-sieve/tree/c8d01549d2ae640b36ec198c1f0f6495f1b036cf","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000021-v1.json","repo":"https://github.com/jasondavies/iwaniec-linear-sieve","tags":["math.NT","msc:11N35","msc:11N36","msc:11N05","msc:11N25","sieve-theory","number-theory","jacobsthal-problem","lean"],"score":0,"title":"Iwaniec's linear sieve at the sifting limit and Jacobsthal's problem","trust":"high","domain":"math.NT","source":"palomar","authors":["Jason Davies"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization of H. Iwaniec, \"On the error term in the linear sieve\" (Acta Arith. 19, 1971) and \"On the problem of Jacobsthal\" (Demonstratio Math. 11, 1978). The headline result is Iwaniec's bound for Jacobsthal's problem: if m consecutive integers are each divisible by one of r ≥ 2 given primes, then m ≤ C (r log r)² for an absolute constant C. More strongly, every interval of length c ∏ (1 − 1/q)⁻¹ r² log r contains at least r² integers coprime to r given primes. Both the Theorem and the Corollary of the 1978 paper are proved, together with its Lemma 1 (the shifted sieve, both…","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 error term in the linear sieve","identifier":"doi:10.4064/aa-19-1-1-30","relationship":"formalizes"},{"title":"On the problem of Jacobsthal","identifier":"doi:10.1515/dema-1978-0121","relationship":"formalizes"}]}