number theory

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

arXiv:2606.24872

summary

The paper solves Erdős Problem 768 by determining the exact leading constant in the asymptotic formula for the proportion of integers whose every prime divisor has a co‑divisor congruent to 1 mod that prime, and the full proof has been formally verified in Lean 4.

Abstract

We resolve ErdÅs Problem 768. Let $A (x)$ count the positive integers $n \leq x$ such that, for every prime $p ∣ n$ , there is a divisor $d > 1$ of $n$ with $d \equiv 1 (mod p)$ . ErdÅs asked whether $A (x) / x = exp (- (c + o (1)) lo g x lo g lo g x)$ for some constant $c > 0$ . We prove that this holds with $c = 1/ (2 lo g 2)$ ; equivalently, $lo g (x / A (x)) / (lo g x lo g lo g x)$ tends to $1/ (2 lo g 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.

20 pages. V2 updated to reflect formal verification of the complete proof in Lean 4 using Aristotle

Topics & keywords

#analytic number theory #erdos problems #divisor conditions #asymptotic analysis #formal verification #proof assistantsA(x)Sylow divisor conditionmultiplicative large sievesubset-product second momentcanonical witness divisorsLean 4

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

Abstract

Topics & keywords

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