A Resolution of Erdős Problem 768: the Sylow Divisor Condition

We resolve Erdős Problem 768. Let $A(x)$ count the positive integers $n\le x$ such that, for every prime $p\mid n$, there is a divisor $d>1$ of $n$ with $d\equiv 1(\mathrm{m}\mathrm{o}\mathrm{d}p)$. Erdős asked whether $A(x)\mathrm{/}x=\exp (-(c+o(1))\sqrt{\log x}\log \log x)$ for some constant $c>0$. We prove that this holds with $c=1\mathrm{/}(2\sqrt{\log 2})$; equivalently, $\log (x\mathrm{/}A(x))\mathrm{/}(\sqrt{\log x}\log \log x)$ tends to $1\mathrm{/}(2\sqrt{\log 2})$. The lower bound is obtained from primes in disjoint logarithmic intervals using a fourth-moment argument based on the multiplicative large sieve and a subset-product second moment. The upper bound uses canonical witness divisors, a deterministic compression map, an injective reconstruction theorem for its fibers, and growing divisor moments. Thus the paper determines the exact leading constant in Erdős Problem 768. The main theorem and its complete proof have been formally verified in the Lean 4 proof assistant.