The board / additive combinatorics / #818
Erdős Problem #818
PROVED LEANdatabase updated 2026-04-25
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).
Let \(A\) be a finite set of integers such that \(\lvert A+A\rvert \ll \lvert A\rvert\). Is it true that \[\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{(\log \lvert A\rvert)^C}\] for some constant \(C>0\)? This was proved by Solymosi [So09d], in the strong form \[\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{\log \lvert A\rvert}.\] See also [52].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/818.Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/818
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.