---

Claim. Let $A$ be the set of integers $n$ for which some representation $1=\sum_{i=1}^k1/m_i$ with $1\le m_1<\cdots<m_k=n$ exists, and $B=\mathbb N\setminus A$. Martin's Theorem 4 states that for every positive rational $r$ the set $\mathcal L_1(r)$ of integers $x>r^{-1}$ that cannot be the largest denominator of an Egyptian fraction representation of $r$ has density zero, and that for $x\ge3$ its counting function satisfies

$$\frac{x\log\log x}{\log x}\ll_r L_1(r;x)\ll_r\frac{x\log\log x}{\log x}.$$

At $r=1$ the set $\mathcal L_1(1)$ is $B$ (the integer $1$ lies in $A$ by the one-term representation), so $|B\cap[1,x]|\asymp x\log\log x/\log x$ and $A$ has density $1$: the answer to the problem's question is yes. The proof also describes $B$: for large $x$, every $n\le x$ with a prime factor exceeding $Cx/\log x$ lies in $B$, and every element of $B$ below $x$ is at most $x/\log x$ or has a prime-power factor exceeding $x\log^{-24}x$, which is the precise form of Martin's remark that the excluded integers are the tiny multiples of prime powers.

Sources. The library card Martin 2000 cites the arXiv text (math/9811112v1, the only arXiv version; no file of it is held) and has the Theorem 4 page, whose statement was read clause by clause and whose proof (pp. 24--25 of the preprint) was read for structure; its inputs, Lemmas 9, 10 and 18, are not compiled, and the journal text was not compared with the preprint. The problem page checks the elementary facts the site's commentary records (closure under multiplication, doubling, no prime power in $A$).

Acceptance. The paper is published in Acta Arithmetica 95 (2000), no. 3, 231--260, a refereed journal (the arXiv listing's journal reference and the Crossref record for DOI 10.4064/aa-95-3-231-260, both), which is the refereed evidence. The site's curator, Thomas Bloom, labels the problem proved and credits the affirmative answer to this paper on the problem page (last edited 20 December 2025); the curator is not an author, and that credit is the reviewed evidence.

Formalization by others. The file src/latest/ErdosProblems/Erdos292.lean of Boris Alexeev's collection plby/lean-proofs, linked above at the pinned commit, declares itself a Lean formalization of the density-one resolution of the problem, names Greg Martin as its informal author and Codex and GPT-5.6 Sol as its formal authors, imports UnitFractions.ErdosProblems and proves erdos_292 : has_density largestDenominators 1. Its proof does not follow Martin's argument: it derives the upper density zero of $B$ from the positive-upper-density theorem erdos298 of that library and gives no counting bound for $B$. The formal-conjectures statement ErdosProblems/292.lean, added on 22 September 2026, tags this file as its formal proof, and the community database lists the problem as formalized as of its last update, of the same date. This corpus has not built or audited the file, so formalized is not listed.