Iwaniec's linear sieve at the sifting limit and Jacobsthal's problem
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000021
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000021/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000021/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'