{"id":"palomar/PALOMAR-2026-10-05-000002","url":"https://github.com/linrock/math-proofs/tree/7caa4144741e10f96cf79d6f7313a0efd9a18b67/erdos-2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-05-000002-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.NT","math.CO","msc:11A07","msc:11B25","covering-systems","number-theory","erdos-problems","lean-formalization"],"score":0,"title":"Erdős 2: minimum modulus of distinct covering systems","trust":"high","domain":"math.NT","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.NT","summary":"A complete Lean 4 proof of the negative answer to Erdős problem 2 (Hough 2015; Balister–Bollobás–Morris–Sahasrabudhe–Tiba 2022): there is an absolute constant B such that every finite covering of the integers by distinct moduli > 1 contains a modulus ≤ B. For any finite set D of moduli above B with N = lcm(D), the proof builds a probability measure on ZMod N prime by prime via the BBMST half-cap fiber update, preserving the progression bound w(z ≡ a mod d) ≤ 2^ω(d)/d while bounding each prime-p loss by C (log p)^6 / (p - 1)^2 via Euler factorization and Mertens' third theorem. Combining this…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-05","reactions":{},"formalized":true,"formalizes":[{"title":"On the Erdős Covering Problem: the density of the uncovered set","identifier":"https://arxiv.org/abs/1811.03547v1","relationship":"adapts"}]}