Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 673
claims/: The 2 claim pages of Problem 673, one per claimant's result; the problem's standing derives from them.
Statement. Let be the divisors of and
Is it true that for almost all ? Can one prove an asymptotic formula for ?
Status. The site labels the problem PROVED; its remarks record Tao's
bounds , displayed for any divisor of
and true for , answering the first question yes, and Erdős's 1982 remark
that the divergence is trivial. The standing in the frontmatter derives from
the claim pages under the parts divergence and asymptotic: the accepted
full claim on
Erdős and Tenenbaum's 1983 paper
settles both questions, its Théorème 2 giving
, and the accepted partial claim on
Erdős's remark settles
the first; the problem is solved with the value proved.
Source. erdosproblems.com/673, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #673, https://www.erdosproblems.com/673.
References.
- [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82.
- [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59-79.
- P. Erdős and G. Tenenbaum, Sur les diviseurs consécutifs d'un entier. Bull. Soc. Math. France 111 (1983), 125--145, doi:10.24033/bsmf.1981.
- Tenenbaum, Gérald, Some of Erdős' unconventional problems in number theory, thirty-four years later (2013), 651--681.
Formalization. Statement in
formal-conjectures,
added on 2026-09-20 and amended on 2026-09-22 to require in Tao's
bound. As amended on 2026-09-22, the file states three results tagged
research solved: erdos_673.parts.i, that for every the set of with
has density ; erdos_673.parts.ii, that
; and erdos_673.variants.average, that
the average of over tends to infinity. Each carries a
formal_proof attribute pointing to the theorem erdos_673 of Boris
Alexeev's repository of formalized Erdős problems at a pinned commit, and
Tao's bound is stated as a textbook variant. A statement file is not a proof:
its own proofs are placeholders. Alexeev's development, which proves both the
divergence for almost all and the asymptotic formula, is linked at a
pinned commit from
Erdős and Tenenbaum's claim page
as a formalization of their result. This corpus built it at that commit,
checked that its theorem Erdos673.erdos_673 uses only the axioms propext,
Classical.choice and Quot.sound and matches its comparator challenge, and
audited the statement, so the claim page lists it as formalized evidence.
Current assessment
The question has two parts. The first, whether for almost all
, is answered yes: for a divisor of every divisor of is
followed in the ordered divisor list by a divisor at most , so
, and with this makes comparable
to for every with a prime factor below a fixed bound; the site
records the argument as Tao's observation, and Erdős's 1982 survey (Chapter
II, section 6, p. 66) calls the divergence trivial while giving no proof.
Erdős and Tenenbaum's 1983 paper gives the same argument on p. 127, with
the least prime factor of . The accepted claims are
theirs, which
settles both parts, and
Erdős's remark. The
second part, an asymptotic formula for , was answered by
Erdős and Tenenbaum, Bull. Soc. Math. France 111 (1983), 125--145, whose
Théorème 2 gives with an explicit error
term; Tenenbaum's 2013 survey sharpens it to
,
where . Erdős's 1979 Luminy paper ([Er79e],
p. 74, where the sum is written ) asks for an asymptotic formula and
calls it easy to prove that ; the 1982
survey says on p. 66 that he hopes to prove that has a
distribution function, and a note on p. 67 adds that he and Tenenbaum proved
in July 1981 that it has a continuous distribution function, a result on the
ratio whose existence part the 1983 paper publishes as Théorème 1, beside the
mean value. A Lean development of August 2026 in Boris Alexeev's repository
proves and is linked from the
Erdős--Tenenbaum claim page as a formalization of their result. The
formal-conjectures statement file linked under Formalization points to that
development as the formal proof of both parts, and the pull request that
added it (#6383,
merged 2026-09-20) records that its author rebuilt the development's closure
against that repository's Mathlib, with #print axioms reporting only
propext, Classical.choice and Quot.sound, and compiled a bridge from the
development's definition of to the file's own statements. This corpus built
the development at a pinned commit of 2026-09-15 and audited its statement,
which the Erdős--Tenenbaum claim page records as formalized evidence beside
the refereed paper; the build certifies the divergence and the leading term of
the mean value, not the paper's error term. The site records Tao's suggestion
that the problem was a slip that Erdős corrected a year later into
Problem 448. The literature search behind
this account, dated 2026-10-07, covered the site's page and discussion thread,
the 1979 paper, the 1982 survey, Erdős and Tenenbaum's 1983 paper, Tenenbaum's
2013 survey, Alexeev's repository and the formal-conjectures file.
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.
- erdos_1982_my_favourite_problems_which_recently_have
- erdos_1979_unconventional_problems_number_theory_asterisque
- tenenbaum_2013_erdos_unconventional_problems_number_theory
- tenenbaum_2013_erdos_unconventional_problems_number_theory / estimate_p9
- weingartner_2015_practical_numbers_distribution_divisors
- weingartner_2015_practical_numbers_distribution_divisors / corollary_1
- weingartner_2015_practical_numbers_distribution_divisors / theorem_1