Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 45
claims/: The 1 claim page of Problem 45, one per claimant's result; the problem's standing derives from them.
Statement. Let . Is there an integer such that, if $D={ 1<d<n_k : d\mid n_k}$, then for any -colouring of there is a monochromatic subset such that ?
Formulation. The site's wording (page last edited 28 September 2025). is the set of nontrivial proper divisors of , so its elements are distinct and is finite. The question asks for one integer for each ; how small can be is a separate quantitative question recorded below.
Status. Proved. Croot's coloring theorem (Annals of Mathematics 157 (2003)) gives an interval every -coloring of which contains a monochromatic set with reciprocal sum one, and can be taken to be the least common multiple of the integers up to . The site records "PROVED (LEAN)"; the Lean suffix is a catalog label whose scope is qualified under Existing formalization below, and no local kernel credit is claimed. The claim page Croot 2003 records the result, its postings and the acceptance evidence (refereed publication and the curator's credit) from which the standing above derives.
Source. erdosproblems.com/45, accessed 2026-09-17: the problem page (PROVED (LEAN); last edited 28 September 2025), its empty discussion thread and its empty proof-claim tab. The site cites [Er95] and [Er96b] as the problem's sources and [Cr03] and [Gu04] in its commentary. Cite as: T. F. Bloom, Erdős Problem #45, https://www.erdosproblems.com/45, accessed 2026-09-17.
References.
- [Cr03] Croot, III, Ernest S., On a coloring conjecture about unit fractions. Ann. of Math. (2) 157 (2003), no. 2, 545--556; arXiv:math/0311421. Library home: croot_2003_coloring_conjecture_about_unit_fractions.
- [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021), v2 (2023); J. Eur. Math. Soc. 27 (2025), 4563--4589. Context: its Theorem 1 restates Croot's coloring theorem and its Theorem 3 gives another admissible . Library home: bloom_2021_density_conjecture_about_unit_fractions.
- [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas 2 (1995), 165--186. Library home: erdos_1995_my_favourite_problems_number_theory_combinatorics; the passage is item 8 of Part I, p. 6.
- [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333--335. Not held; no library home.
- [Gu04] Guy, Richard K., Unsolved problems in number theory, third edition, Problem Books in Mathematics, Springer (2004), xviii+437 pp.; B2 "Almost perfect, quasi-perfect, pseudoperfect, harmonic, weird, multiperfect and hyperperfect numbers", printed p. 80, the section the site cites: Erdős defines as the smallest integer such that any partition of its proper divisors into classes has as a sum of distinct divisors from one class, with (from ) and the existence of unproved. This is a closely related divisor-sum form, not the same question: under it also colors the divisor , which corresponds to the term that the site's excludes, so Guy's need not equal the site's (for , has no subset with reciprocal sum one). Existence for every agrees between the two forms. Library home: guy_2004_unsolved_problems_number_theory.
Formalization. Statement in
ErdosProblems/45.lean
of formal-conjectures at the linked revision, with an external proof tag
pointing at a Lean 4 file in another collection; this corpus has built or
checked neither. See Existing formalization.
Current assessment
The question. On 2026-09-17 the site asks, for each , for an integer whose nontrivial proper divisors cannot be -colored without a monochromatic set of reciprocal sum one, shows PROVED (LEAN), and explains in its commentary that this follows from Croot's coloring theorem with for some constant (take to be the least common multiple of an interval ), that a doubly exponential lower bound also holds (an observation the commentary attributes to Sawhney), and that Guy's collection mentions the existence of such in problem B2. The thread and the proof-claim tab are empty. The community database record (teorth/erdosproblems,) says proved (Lean), statement formalized, no formal-proof URL.
Status support. The status-defining source is Croot's Corollary (result page), printed p. 545 of arXiv:math/0311421v1, which carries the Annals of Mathematics pagination 545--556 and the received date 16 May 2001; the journal is refereed and the arXiv listing shows no later version. The Corollary gives a constant such that every partition of into classes has a class containing a set with reciprocal sum one, with for large . The specialization to this problem is the common-multiple construction written on the Corollary page: with and , every integer of is a nontrivial proper divisor of , so a -coloring of restricts to a -coloring of and the Corollary supplies . This specialization is elementary and unreviewed. The statements of the Corollary and of the Main Theorem behind it are compiled (claims checked); Croot's proof (Sections 2--6, pp. 548--555) has not been compiled, which is the remaining proof-coverage obligation.
Quantitative remarks, not status. The construction gives by the prime number theorem, the site's . The site's commentary sketches a matching lower bound : the divisors of must have reciprocal sum at least , or a greedy coloring is a counterexample, which by Mertens's theorem forces the product of the primes dividing to be at least doubly exponential in . This is site commentary attributed to Sawhney, not a refereed result, and its packing step is unverified. Any theorem that produces a unit subsum from a reciprocal mass of size , such as Bloom's Theorem 3 or Liu and Sawhney's Theorem 1.1, also yields an admissible by the same construction, because one of the color classes of has reciprocal mass above ; these routes give other values of , not a smaller order of growth.
Search scope. The problem, discussion and proof-claim pages; the community database record; the formal-conjectures file at the pinned commit and the external Lean file it tags; the arXiv listing for math/0311421 (one version; journal reference "Ann. of Math. (2), Vol. 157 (2003), no. 2, 545--556"); the Annals article page; the Semantic Scholar citing-paper records for Croot's paper (twenty records, of which the 2025 and 2026 items concern approximate reciprocal subsums, faithful decompositions of rationals and Rado numbers, none this problem); the arXiv API listing of the sixty most recent abstracts mentioning unit or Egyptian fractions (to 7 September 2026; none concerns this problem); and two general web searches. Not searched: MathSciNet, zbMATH, full-text search engines for scholarly literature, X. Nothing found changes the status or improves the doubly exponential order of .
Remaining gaps. Croot's proof is not compiled (statements only). The passage of [Er95] is item 8 of Part I, p. 6; [Er96b] is not held and has no library home; the [Gu04] passage is B2, printed p. 80. The lower-bound sketch is unverified. The Lean files were not built.
Progress and known results
The Corollary of Croot's paper states: there exists a constant so that for every partition of the integers in into classes, one class contains a subset with ; works for sufficiently large, and cannot be smaller than . It follows from the Main Theorem, a unit-subsum criterion for sets of smooth integers in with reciprocal mass above , through the reciprocal-mass estimate (1.1) for the smooth integers in .
Taking answers the question, as written on the Corollary page. The same coloring theorem answers Problem 46, the coloring of all integers, and the density strengthening is Problem 298. The quantitative threshold question for reciprocal masses is Problem 47.
Existing formalization
The formal-conjectures file ErdosProblems/45.lean, at the revision the
Formalization link above pins, declares
erdos_45 : answer(True) ↔ ∀ k : ℕ, 2 ≤ k → ∃ n : ℕ, ∀ c : ℕ → Fin k, ∃ a : Fin k, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', c d = a) ∧ D'.reciprocalSum = 1
(the file's two bound variable names for the coloring and the color are
shortened to c and a here) under category research solved, with proof
sorry and the attribute
formal_proof using lean4 at the file
src/v4.29.1/ErdosProblems/Erdos45.lean of the collection
plby/lean-proofs. That file
(Erdos45.lean,
at the pinned revision) names Croot as informal author and Bhavik Mehta and
Thomas Bloom as formal authors with the URL of the Bloom–Mehta repository,
imports ErdosProblems.Erdos46 and
Mathlib.Combinatorics.Compactness, and proves
erdos45 : ∀ k : ℕ, 2 ≤ k → ∃ nₖ : ℕ, ∀ c : ℕ → Fin k, ∃ D' : Finset ℕ, D' ⊆ ((nₖ.divisors.erase 1).erase nₖ) ∧ rec_sum D' = 1 ∧ ∃ a : Fin k, ∀ d ∈ D', c d = a
without sorry, ending with a comment that records #print axioms erdos45
as propext, Classical.choice, Quot.sound. Its Erdos46.lean imports
ErdosProblems.Erdos298, the collection's file for Problem 298 (Bloom's
density theorem), so the formal route runs through the density theorem
rather than through Croot's argument. The collection's README says its
source subdirectories "build as a whole (last I checked)". This corpus has
built, audited or kernel-checked none of it; the site's Lean suffix is a
catalog label, the community database records no formal-proof URL, and the
statements above are the only formal content this page rests on.
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.