REVIEW 4 minor 12 references
A Resolution of Erd\H{o}s Problem 768: the Sylow Divisor Condition
T0 review · 0 major / 4 minor · reviewed 2026-07-14 · grok-4.5
Pith's one-line read The density of integers with a Sylow-style witness divisor for every prime factor decays as exp(−(1/(2√log 2)+o(1))√(log x) log log x).
desk verdict Exact constant for Erdős 768 is proved two-sided; the written argument holds and the Lean claim is the only unreproducible bit. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The matching of two exponential rates: a fourth-moment large-sieve cleaning of logarithmic prime layers plus a subset-product second-moment lemma for the lower bound, and a deterministic compression map n↦n/Q(n) whose fibers are injectively reconstructed from a half-row record and then bounded by growing divisor moments for the upper bound; optimizing max{λ/2, λ/4 + 1/(4λ log 2)} yields the constant.
What would settle it
Compute the ratio log(x/A(x)) / (√(log x) log log x) for successive large x (or check the Lean formalization of the main theorem and its complete proof) and see whether it approaches 1/(2√log 2).
Extended reading notes
Core claim
The limit lim log(x/A(x)) / (√(log x) log log x) equals 1/(2√log 2), so A(x)=x exp(−(1/(2√log 2)+o(1))√(log x) log log x). Both the lower-bound construction from cleaned logarithmic prime layers and the upper-bound compression by canonical witnesses optimize to this same constant.
Load-bearing premise
After the large sieve is applied to products of primes from each logarithmic layer, only an exponentially small set of target primes can still have a large Fourier coefficient; without that cleaning the constructive lower bound cannot reach the matching constant.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper resolves Erdős Problem 768 by proving that if A(x) counts n ≤ x such that every prime p dividing n admits a divisor d > 1 of n with d ≡ 1 (mod p), then lim log(x/A(x)) / (√(log x) log log x) = 1/(2√log 2). Equivalently A(x) = x exp(−(1/(2√log 2) + o(1)) √(log x log log x)). The lower bound selects one prime from each of r disjoint logarithmic intervals, cleans exceptional Fourier coefficients via a fourth-moment application of the multiplicative large sieve (Lemma 4.2 + Theorem 2.6), and applies a subset-product second-moment lemma (Lemma 3.1) to guarantee witnesses; the resulting counting loss r log r + r log log r produces the constant. The upper bound fixes canonical witnesses D_p, extracts a binary-homogeneous subsequence by majority-halving, builds a deterministic square-free compression factor Q(n), proves injectivity of the fibers of n ↦ n/Q(n) by an explicit reconstruction record (Propositions 6.7–6.11), and bounds the fibers by growing divisor moments (Lemmas 2.2–2.3); optimizing the two exponential rates over λ = ω(n)/√log x recovers the same constant.
Significance. If correct, the result completely settles a classical Erdős problem by identifying the precise leading constant rather than merely establishing the conjectural shape. The matching of independent lower- and upper-bound constants, the clean use of the multiplicative large sieve for Fourier uniformity, and the novel deterministic compression/reconstruction apparatus are genuine technical contributions. The claimed complete formal verification of the main theorem and its proof in Lean 4 is a substantial additional strength that raises the reliability bar for the analytic argument. The work also supplies a sharp elementary upper bound on the possible orders of non-abelian finite simple groups, linking analytic number theory to group theory.
minor comments (4)
- [Abstract / §1] Abstract and introduction assert that the main theorem and complete proof have been formally verified in Lean 4, yet the manuscript contains no repository link, commit hash, or artifact pointer. Adding a stable reference would allow readers to inspect the formalization.
- [§4, Remark 4.1] The safety margins 10 and 8 appearing in the definitions of v and δ (Eq. (4.1)) are described as “convenient” but never quantified further; a one-sentence remark that any sufficiently large absolute constants work would clarify that the specific numbers are not essential.
- [§2, Lemma 2.2] Lemma 2.2 encodes vectors by subset multiplicities; the injection into weak compositions is correct, but a parenthetical reference to the standard stars-and-bars identity would make the counting step more transparent to non-specialists.
- [§6] In the reconstruction lemmas (6.4–6.6) the bookkeeping of “exact” versus “visible” slots is dense; a short schematic table (already partially present in Remark 6.8) placed earlier would improve readability.
Circularity Check
No circularity: matching constant arises from independent lower-bound construction and upper-bound optimization, not by definition or self-citation.
full rationale
The derivation is self-contained analytic number theory. The lower bound constructs n as a product of one prime from each of r disjoint logarithmic intervals (after large-sieve fourth-moment cleaning of exceptional Fourier coefficients), applies a subset-product second-moment lemma to obtain witnesses, and obtains log n ~ (log 2) r^{2} against an r log r counting loss, yielding the constant 1/(2√log 2). The upper bound uses deterministic canonical witnesses, majority-halving homogeneous sequences, a compression map n ↦ n/Q(n), an injective fiber reconstruction, and growing divisor moments; the resulting rates λ/2 and λ/4 + 1/(4λ log 2) are optimized over λ to the identical value. Neither side defines the target constant into its inputs; background tools (multiplicative large sieve, PNT, character orthogonality, divisor bounds) are standard external theorems. No fitted parameters, no load-bearing self-citations, and no renaming of a known empirical pattern occur. The claimed Lean formalization is an external verification claim, not part of the written derivation chain.
Assumptions & free parameters
free parameters (3)
- safety margin 10 in v := α(r−1) − 10 log r
- safety margin 8 in δ := 8α / log r
- additive constant 3 in H_t := ⌈log(t+2)/(2 log 2)⌉ + 3
assumptions (4)
- standard math Multiplicative large sieve (Bombieri–Davenport form): ∑_{q≤Q} (q/φ(q)) ∑* |∑ a_n χ(n)|² ≪ (N+Q²) ∑ |a_n|²
- standard math Prime-number theorem with classical zero-free-region error: π(y) = li(y) + O(y e^{−c√log y})
- standard math Character orthogonality on finite abelian groups and Dirichlet characters modulo primes
- domain assumption Existence of a minimal witness divisor D_p(n) for each prime p | n when n ∈ A
invented entities (2)
-
Canonical witness divisor D_p(n)
-
Deterministic compression map n ↦ n/Q(n) built from a majority-halving homogeneous subsequence
Cite this review
Pith. "Pith review of A Resolution of Erd\H{o}s Problem 768: the Sylow Divisor Condition." pith.science (2026). https://pith.science/paper/LKEJW6XE
@misc{pith2026260624872,
author = {Pith},
title = {Pith review of: A Resolution of Erd\Hos Problem 768: the Sylow Divisor Condition},
year = {2026},
howpublished = {\url{https://pith.science/paper/LKEJW6XE}},
note = {Machine review of arXiv:2606.24872}
}
abstract
We resolve Erd\H{o}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\H{o}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\H{o}s Problem 768. The main theorem and its complete proof have been formally verified in the Lean 4 proof assistant.
Reference graph
Works this paper leans on
-
[1]
Bombieri and H
E. Bombieri and H. Davenport, Some inequalities involving trigonometrical polynomials,Ann. Scuola Norm. Sup. Pisa Cl. Sci. (3)23(1969), 223–241
1969
-
[2]
Dornhoff, Simple groups are scarce,Proc
L. Dornhoff, Simple groups are scarce,Proc. Amer. Math. Soc.19(1968), 692–696
1968
-
[3]
L. Dornhoff and E. L. Spitznagel, Jr., Density of finite simple group orders,Math. Z.106(1968), 175–177, doi:10.1007/BF01110127
-
[4]
Erdős, Remarks on some problems in number theory,Mathematica Balkanica4(1974), 197–202
P. Erdős, Remarks on some problems in number theory,Mathematica Balkanica4(1974), 197–202. Available at https://www.renyi.hu/~p_erdos/1974-27.pdf
1974
-
[5]
T. F. Bloom, Erdős Problem 768,https://www.erdosproblems.com/768, accessed 19 June 2026
2026
-
[6]
J. F. Hurley and A. Rudvalis, Finite simple groups,Amer. Math. Monthly84(1977), 693–714, doi:https: //doi.org/10.1080/00029890.1977.11994461
-
[7]
Iwaniec and E
H. Iwaniec and E. Kowalski,Analytic Number Theory, American Mathematical Society Colloquium Publications, vol. 53, American Mathematical Society, Providence, RI, 2004
2004
- [8]
Show all 12 references
-
[9]
H. L. Montgomery and R. C. Vaughan,Multiplicative Number Theory I: Classical Theory, Cambridge Studies in Advanced Mathematics, vol. 97, Cambridge University Press, Cambridge, 2007
2007
-
[10]
OEIS Foundation Inc., Sequence A352287,The On-Line Encyclopedia of Integer Sequences,https://oeis.org/ A352287, accessed 19 June 2026
2026
-
[11]
On the density of the orders excluded by the Sylow theorems for simple groups,
W. Sawin, Answer to “On the density of the orders excluded by the Sylow theorems for simple groups,” MathOverflow(11 September 2021), MathOverflow answer, accessed 19 June 2026
2021
-
[12]
E. L. Spitznagel, Jr. and S. A. Szygenda, A computer study of the orders of finite simple groups,Math. Comp. 22(1968), 669–671, doi:10.1090/S0025-5718-1968-0227266-5
1968 doi
Reviewed July 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.