Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 419
claims/: The 1 claim page of Problem 419, one per claimant's result; the problem's standing derives from them.
Statement. If counts the number of divisors of , then what is the set of limit points of
Status. The site labels the problem SOLVED (LEAN). The standing derived
from the claim page is solved, answered: the limit points are exactly
and the numbers for , by
Erdős, Graham, Ivić and Pomerance 1996,
credited by the site's curator. The Lean proof the site's label refers to is
third-party work not built here.
Source. erdosproblems.com/419, accessed 2026-09-04 and 2026-10-07; the problem page was last edited 14 October 2025. The site cites the problem from p. 83 of Erdős and Graham's 1980 problem book [ErGr80], where Erdős and Graham state that every is a limit point and that they cannot exclude others. Cite as: T. F. Bloom, Erdős Problem #419, https://www.erdosproblems.com/419.
References.
- [EGIP96] Erdős, Paul and Graham, S. W. and Ivić, Aleksandar and Pomerance, Carl, On the number of divisors of . Analytic Number Theory, Birkhäuser Boston (1996), 337-355. Library home: erdos_1996_number_divisors.
- [ErGr80] Erdős, P. and Graham, R. L., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique 28, Université de Genève (1980), p. 83. Library home: erdos_1980_old_new_problems_results_combinatorial_number_theory.
Formalization. The formal-conjectures file
FormalConjectures/ErdosProblems/419.lean
(commit of 2026-09-18) states the set of limit points as
erdos_419 with sorry, tags it solved and names as its formal proof, by an
unpinned link, the file Erdos419.lean of Boris Alexeev's repository of Lean
proofs; the claim page links that file at a pinned commit. Nothing has been
built here.
Current assessment
The question, as the site states it (page last edited 14 October 2025): what is the set of limit points of , where counts divisors? The answer is .
The resolution. Erdős, Graham, Ivić and Pomerance [EGIP96] prove that
with the largest prime
factor of (Theorem 2), and deduce the set of limit points (Corollary 1):
is always for the integer , each occurs
infinitely often, and these values accumulate only at . Erdős and Graham
had known that every is a limit point and asked whether there are
others; there are none. The site's page carries an argument attributed to
Mehtaab Sawhney that reaches the same set by factoring the ratio over the
primes dividing , and the curator records that the paper of 1996 already
contains essentially that argument. The
claim page
records the theorem, the site's argument and the acceptance: a published
paper credited by the site's curator; it appeared in a conference volume, so
no refereed evidence is listed. The same paper's bounds on how far one must
go for the divisor count of a factorial to double bear on
Problem 420.
Search scope, 2026-10-07: the site's problem page, its discussion thread (one post, of 2026-01-31, announcing the Lean proof) and its proof-claims page, which lists no proof claim for the problem; the formal-conjectures statement file at the commit the Formalization field links; and the Lean file in Alexeev's repository at the commit the claim page links. Neither Lean file has been built here.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.