Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. For every there is an integer such that every -coloring of the set of nontrivial proper divisors of has a monochromatic subset with . The answer to Problem 45 is yes.
Result. Croot's Corollary (Annals of Mathematics (2) 157 (2003), no. 2, 545--556, printed p. 545; paged at corollary) gives a constant such that every partition of the integers in into classes has a class containing a finite set with reciprocal sum one, with admissible for large . The specialization to this problem is elementary and is 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 . Croot's paper does not state Problem 45 itself; the site's commentary records this deduction and credits Croot with the result. The construction gives , and the site's commentary sketches a matching doubly exponential lower bound that is unverified.
Depends on. Croot's Corollary, the result page of the cited paper, which also writes out the specialization to this problem.
Acceptance. Refereed: the paper appeared in the Annals of Mathematics, received 16 May 2001, issue dated March 2003; the arXiv text (arXiv:math/0311421v1, 24 November 2003) is the published version with the journal pagination. Reviewed: the site's curator, Thomas Bloom, marks the problem proved and credits Croot's theorem in the commentary, an acceptance independent of the claimant. The library holds Croot's Corollary and Main Theorem as checked statements; the proof (Sections 2--6, pp. 548--555) is not rewritten in the library and has no independent review there, which is a proof-coverage gap, not a doubt about the result.
Formalization. The linked Lean 4 file declares itself a formalization
of a solution to Problem 45, names Croot as its informal author and Bhavik
Mehta and Thomas Bloom as its formal authors, and proves, without sorry,
that for every some has the property above for every coloring
of the naturals with colors; its recorded axioms are propext,
Classical.choice and Quot.sound. Its route runs through the
collection's file for Problem 46
and from there through Bloom's density theorem
(Problem 298), not through Croot's
argument. This corpus has not built or audited that file, so it is a
posting of the result, not formalized evidence here; the site's Lean
suffix is a catalog label. The formal-conjectures statement file
for the problem is a statement with a sorry body and is not a
formalization of the result.