A Resolution of Erdős Problem 768: the Sylow Divisor Condition
Eric Li
math.NT
Jun 23, 2026 · v2
TL;DR
The main theorem on Erdős Problem 768 is fully formalized in Lean 4 over Mathlib, produced with Harmonic's Aristotle and audited by the author, building on PrimeNumberTheoremAnd.
Abstract
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 \pmod p$. Erdős asked whether $A(x)/x=\exp(-(c+o(1))\sqrt{\log x}\log\log x)$ for some constant $c>0$. We prove that this holds with $c=1/(2\sqrt{\log 2})$; equivalently, $\log(x/A(x))/(\sqrt{\log x}\log\log x)$ tends to $1/(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.
Problem
Erdős Problem 768 asks whether the density of integers n, such that every prime p dividing n has a divisor d>1 of n with d ≡ 1 mod p, decays like exp(-(c+o(1))√(log x) log log x) for some constant c>0.
Approach
The lower bound uses primes in disjoint logarithmic intervals, cleaned with a fourth-moment argument based on the multiplicative large sieve, together with a subset-product second-moment lemma over finite abelian groups. The upper bound uses canonical witness divisors, a deterministic compression map, an injective reconstruction theorem for its fibers, and growing divisor moments. The full proof was formalized in Lean 4 with Mathlib, using the MediumPNT theorem from the PrimeNumberTheoremAnd project as the analytic input.
Results
The asymptotic holds with exact constant c = 1/(2√(log 2)). The Lean statement Erdos768.erdos_768 matches the theorem, contains no sorry, and depends only on the standard axioms. This is checked by continuous integration.
