---

Claim. For every infinite set $A$ of positive integers, with $A(n)=\lvert A\cap[1,n]\rvert$, there is a set $B$ such that $A+B$ contains every sufficiently large integer and

$$B(n)\le C\sum_{k=1}^{n}\frac{\log A(k)}{A(k)},$$

with $C$ absolute and a term with $A(k)=0$ replaced by $1$. Since $A(k)\to\infty$, the summands tend to zero and so does their Cesàro mean, so $B(n)=o(n)$: $B$ has density zero. This proves the statement of Problem 31, the conjecture of Erdős and Straus. The result is Theorem 1 of Lorentz, G. G., On a problem of additive number theory, Proc. Amer. Math. Soc. 5 (1954), no. 5, 838--841, received 1954-03-02 (the page's date) and published in the October 1954 issue; the card lorentz_1954_problem_additive_number_theory records the source, and its page Theorem 1 reconstructs the greedy interval cover, the dyadic assembly and the Cesàro step. If $0\in\mathbb{N}$, apply the theorem to the infinite positive part of $A$; its complement is also one for $A$.

Acceptance. The refereed evidence is the journal publication cited above. The reviewed evidence is the documented acceptance by the catalog erdosproblems.com, whose page for the problem (the first discussion link) carries the label PROVED (LEAN) and its curator, Thomas Bloom, credits Lorentz's paper with the proof. The second discussion link is the catalog's thread, where an exposition of Lorentz's proof (2025-11-22) and the announcement of the Lean formalization below (2025-11-24) were posted.

Formalization. A third party formalized the theorem: erdos_31 in src/v4.29.1/ErdosProblems/Erdos31.lean of Boris Alexeev's repository https://github.com/plby/lean-proofs, pinned above at the commit of 2026-06-24, the file's last change. Its header declares it a formalization of a solution to the problem, names Lorentz, Wouter van Doorn and ChatGPT 5.1 Pro as the informal authors and Aristotle and Boris Alexeev as the formal authors, so it is a formalization of this result and not an independent proof; the formal-conjectures catalog tags its own statement erdos_31 as research solved and links this file. Its statement gives, for every infinite $A\subseteq\mathbb{N}$, a set $B$ of density zero and an $n_0$ with $n\in A+B$ for all $n\ge n_0$, through the file's own HasDensity on $\mathbb{N}$; the file imports only Mathlib. This corpus has not built the file, printed its axioms or audited its definitions, so the claim carries no formalized evidence and the formalization is a link, not a warrant.