---

Claim. Let $A,B\subseteq\mathbb N$ be infinite sets such that the number $r(x)$ of integers up to $x$ outside $A+B$ is $o(x)$ (a wider class than additive complements, for which $r(x)$ is bounded), with $A(x)B(x)/x\to1$, and let the roles be fixed by Narkiewicz's dichotomy so that $A(2x)/A(x)\to1$ and $B(2x)/B(x)\to2$. Write $a^*(x)=\max(A\cap[1,x])$. Theorem 1.2 of I. Z. Ruzsa, Exact additive complements, states that if $r(x)=o(a^*(x))$ then

$$A(x)B(x)-x>(1-o(1))\frac{a^*(x)}{A(x)}.$$

For the sets of Problem 785 the function $r(x)$ is bounded, since $A+B$ contains every large integer, and $a^*(x)\to\infty$, so the hypothesis holds; Narkiewicz's dichotomy gives $A(x)<a^*(x)^\varepsilon$ for large $x$, so the right side tends to infinity and $A(x)B(x)-x\to\infty$, the problem's statement, which Sárközy and Szemerédi had proved (their claim page) and which Ruzsa's introduction records as known. The bound rules out $A(x)B(x)-x=O(A(x)^c)$ for every constant $c$, which Chen and Fang had shown (their claim page). Ruzsa writes that the proof of Theorem 1.2 is based on Chen and Fang's argument, with some parts improved, and it uses Narkiewicz's dichotomy. Theorem 1.3 shows the bound is nearly best possible: for any $\omega(x)\to\infty$ there are exact complements with $A(x)B(x)-x<\min(\omega(x),c\,a^*(x))$ for infinitely many $x$, so no absolute lower bound such as $\log x$ holds. Library home ruzsa_2017_exact_additive_complements (its digest records Theorems 1.1 to 1.3; no proof check is recorded).

Postings. arXiv:1510.00812, submitted 3 October 2015, which names this page; The Quarterly Journal of Mathematics, published online 13 October 2016 (volume 68 of 2017, pp. 227--235, as the problem page cites it). On 7 March 2026 van Doorn posted in the site's discussion thread a Lean formalization of Ruzsa's proof, produced by Aristotle from van Doorn's write-up of the papers of Narkiewicz and Ruzsa, in the Lean-files repository: the module proves narkiewicz_dichotomy, theorem_estimate (Ruzsa's bound) and corollary_erdos_785, the problem's statement for infinite exact complements of positive integers, under its own definitions (the module imports only Mathlib and declares no axiom at the linked commit of 2026-03-07; the corpus has not built it). The formal-conjectures catalog's statement file 785.lean marks erdos_785 solved with that module as its formal_proof link, attributing the Lean proof to van Doorn working with Aristotle (file commit of 2026-09-18, accessed 2026-10-07).

Depends on. Nothing in this wiki.

Acceptance. Refereed: The Quarterly Journal of Mathematics, doi:10.1093/qmath/haw029 (Crossref record accessed 2026-10-07). Reviewed: the site's curator, Thomas Bloom, labels the problem PROVED (LEAN) and credits Ruzsa's bound and construction, as [Ru17], in the problem page's commentary; the curator had no part in the result. The site's Lean qualifier and the catalog's solved marker rest on the formalization above, which the corpus has not built, so formalized is not listed.