Erdős 1139: large gaps between almost-primes

Linmiao Xu

Palomar Registrypalomar/PALOMAR-2026-10-06-000001Oct 6, 2026math.NTscore 0

A Lean 4 formalization of unconditional bounds and conditional reductions for Erdős problem 1139 on consecutive P_2 almost-primes (Ω(u_k) ≤ 2). Extending Chojecki's (2026) Erdős 689 double-covering construction via protected-reserve omission, it proves unconditionally that limsup (u_{k+1} - u_k) / log(k + 1) ≥ A > 1 and that every large height X contains an almost-prime-free interval of length ≥ c log X (c > 1), alongside the mixed prime/prime-square CRT bridge, PNT primorial asymptotics, and squared-core deficiency classification. Using a squared-prime core and scale-adaptive dyadic prime…

SourceRepositoryJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-06-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000001/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-06-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'