---

Claim. Croot's Main Theorem (On unit fractions with denominators in short intervals, Acta Arith. 99 (2001), no. 2, 99--114; arXiv:math/9904181, 30 April 1999): for every rational $r>0$ and every $N>1$ there are integers $N<x_1<\cdots<x_k\le(e^r+O_r(\log\log N/\log N))N$ with $r=1/x_1+\cdots+1/x_k$, and the error term is best possible. Its introduction poses the question of Problem 284 in the corrected form $\max\{x_1\}\sim k/(e-1)$ and says that the theorem answers it for infinitely many $k$. The site marks the problem PROVED and credits the theorem with its solution; the claim's full scope rests on that credit.

Deduction. Take $r=1$. A representation with denominators in $(N,(e+o(1))N]$ has $k>N$ terms, since each term is below $1/N$, and $k\le(e-1+o(1))N$ terms, since the denominators are distinct integers of that interval; so $f(k)\ge x_1>N\ge(1-o(1))k/(e-1)$ for every $k$ that occurs as such a term count, and these $k$ are infinitely many. With the trivial bound $f(k)\le(1+o(1))k/(e-1)$ of the problem page this gives the asymptotic for those $k$, which is the form the paper states.

Acceptance. The paper is published in Acta Arithmetica, a refereed journal (Crossref record of DOI 10.4064/aa99-2-1), which is the refereed evidence. The site's curator, Thomas Bloom, who is independent of the author, marks the problem PROVED and credits Croot's theorem in the commentary, calling the problem essentially solved by it, which is the reviewed evidence. Proof coverage: the proof was read for structure only, on the preprint (Propositions 1 and 2, Lemmas 1--4), and not verified here; the published proof was not compared with the preprint's.

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-17, pinned to the commit of 2026-09-15), whose header names Croot as the informal author and Codex and GPT-5.6 Sol as the formal authors. Its theorem erdos_284 defines $f(k)$ literally as the greatest first denominator over strictly increasing $k$-term representations of $1$ and proves $f(k)/k\to1/(e-1)$; the file contains no sorry. The corpus has not built or audited it, so the claim lists no formalized evidence. formal-conjectures holds no statement file for the problem, and the community database records it as unformalized.

Depends on. No page of this wiki: the deduction uses only the theorem's statement.

Related. The same theorem is the source of the accepted partial claim Croot 1999 on Problem 286, the width question of the same passage of the 1980 monograph.