---

Claim. Every finite coloring of the integers has a monochromatic solution of $1=\sum1/n_i$ with $2\le n_1<\cdots<n_k$. The answer to Problem 46 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 $b$ such that every partition of the integers in $[2,b^r]$ into $r$ classes has a class containing a finite set with reciprocal sum one; $b=e^{167000}$ is admissible for large $r$, and $b\ge e$ is necessary. A coloring of the integers with $r$ colors restricts to such a partition of $[2,b^r]$, so a monochromatic solution exists; listing it increasingly gives $2\le n_1<\cdots<n_k$, and the colors of integers below $2$ play no role. The restriction step is written on the Corollary page. Croot's abstract states the theorem as the coloring statement, which is the form Erdős and Graham conjectured, so the paper claims this result directly. It rests on the paper's Main Theorem, a unit-subsum criterion for heavy sets of smooth integers in a short range.

Acceptance. Refereed: the paper appeared in the Annals of Mathematics, received 16 May 2001, issue dated March 2003; the retained 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 in the commentary, an acceptance independent of the claimant; Bloom's own paper (2021) also quotes Croot's theorem as its Theorem 1 and derives it again from the density theorem, a second route recorded on Bloom's claim page. The library holds the Corollary and the Main Theorem as checked statements; Croot's proof (Sections 2--6, pp. 548--555) is not rewritten in the library and has no independent review there, a proof-coverage gap and not a doubt about the result.

Formalization. The linked Lean 4 file declares itself a formalization of a solution to Problem 46, names Croot as its informal author and Bhavik Mehta and Thomas Bloom as its formal authors, and proves, without sorry, that every coloring of the integers by a finite type has a monochromatic finite set of naturals, all at least $2$, with reciprocal sum one; its recorded axioms are propext, Classical.choice and Quot.sound. Its route is the density route: it imports the collection's file for Problem 298, Bloom's density theorem, not Croot's argument. This corpus has not built or audited that file, so it is a posting of the result and not formalized evidence here; the site's Lean suffix is a catalog label. The formal-conjectures statement file for the problem carries a sorry body and two statement-only variants and is not a formalization of the result.