---

Claim. Martin's Theorem 2 (Denser Egyptian fractions, Acta Arith. 95 (2000), no. 3, 231--260; arXiv:math/9811112, 18 November 1998): for every positive rational $r$ and every integer $t\ge t_0(r)$, the least largest denominator $M_t(r)$ in a $t$-term representation of $r$ by distinct unit fractions satisfies

$$M_t(r)=\frac{t}{1-e^{-r}}+O_r\Bigl(\frac{t\log\log3t}{\log3t}\Bigr),$$

and the order of the error term cannot be lowered. At $r=1$, with $t_0(1)=3$ and $1/(1-e^{-1})=e/(e-1)$, this is $f(k)=\frac{e}{e-1}k+O(k\log\log k/\log k)$ for the $f$ of Problem 285, so the answer to the question is yes for every $k\ge3$, with an explicit error term in place of the $o(1)$.

Acceptance. The paper is published in Acta Arithmetica, a refereed journal (the arXiv listing's journal reference and the Crossref record of DOI 10.4064/aa-95-3-231-260, both accessed), which is the refereed evidence; the author writes (p. 2 of the preprint) that the theorem completely resolves the question of Erdős and Graham. The site's curator, Thomas Bloom, marks the problem PROVED (LEAN) and credits Martin's paper in the commentary, which is the reviewed evidence. Proof coverage: the reduction of Theorem 2 to Propositions 5 and 6 (pp. 4--5 of the preprint) is recorded on the theorem page; the proofs of the propositions (Sections 3--5) have not been checked, and the corpus records no check of the theorem. Locators are those of the arXiv preprint; the journal text has not been compared.

Formalization. The formalization link is a public Lean 4 proof of the problem's statement in Boris Alexeev's lean-proofs repository (file of 2026-08-15, header of 2026-08-23, pinned to the commit of 2026-09-15). Its header calls it a Lean formalization of the resolution of Problem 285 and names Greg Martin as the informal author and Codex and GPT-5.6 Sol as the formal authors; its theorem erdos_285 restates the formal-conjectures statement without the answer(True) wrapper and derives it from the repository's own formalization of Martin's upper bound (Erdos285/MartinUpperFinal.lean), with no sorry. This is the Lean proof behind the site's label PROVED (LEAN) and the community database's formal status Lean since 23 August 2026; the formal-conjectures statement file itself has proof sorry and no pointer to it. The corpus has not built or audited the development, so the claim lists no formalized evidence.