The board / additive combinatorics / #785
Erdős Problem #785
exact additive complements
PROVED LEANdatabase updated 2026-03-06
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The counting function \(A(x)=\lvert A\cap [1,x]\rvert\).
The largest element of \(A\) in \([1,x]\), that is \(a^*(x)=\max A\cap [1,x]\) (equal to \(0\) when there is no such element).
Two sets \(A, B\subseteq \mathbb{N}\) are *exact additive complements* if \(A+B\) contains all large integers and \(A(x)B(x)\sim x\).
Let \(A,B\subseteq \mathbb{N}\) be infinite sets of positive integers such that \(A+B\) contains all large integers. Let \(A(x)=\lvert A\cap [1,x]\rvert\) and similarly for \(B(x)\). Is it true that if \(A(x)B(x)\sim x\) then \[A(x)B(x)-x\to \infty\] as \(x\to \infty\)? A conjecture of Erdős and Danzer. The answer is yes, proved by Sárközy and Szemerédi [SaSz94], who actually proved that it is impossible for \[A(x)B(x)-x=o(A(x)).\] This was formalized in Lean by van Doorn using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 9 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/785.Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/785
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.