---

Claim. The answer to Problem 818 is yes, with $C=1$. The claimed result is Theorem 2.1 of J. Solymosi, Bounding multiplicative energy by the sumset: for every finite set $A$ of positive reals,

$$\lvert AA\rvert\,\lvert A+A\rvert^2 \ge\frac{\lvert A\rvert^4}{4\lceil\log\lvert A\rvert\rceil},$$

so if $\lvert A+A\rvert\le K\lvert A\rvert$ then

$$\lvert AA\rvert\ge\frac{\lvert A\rvert^2}{4K^2\lceil\log\lvert A\rvert\rceil},$$

the site's inequality with one logarithm in place of a power of the logarithm. The bound on $\lvert AA\rvert\,\lvert A+A\rvert^2$ is sharp up to the logarithm, as $A=\{1,\ldots,n\}$ shows. The proof covers $A\times A$ by the lines through the origin and uses that the sumsets of points on consecutive rays are disjoint inside $(A+A)\times(A+A)$; the digest is on the source card. The site asks about finite sets of integers, which may contain $0$ and numbers of both signs; the nonzero members of one sign number at least $(\lvert A\rvert-1)/2$, negating them changes neither the size of the sumset nor the size of the product set, and both sizes are monotone under taking subsets, so the theorem for positive reals gives the integer statement with a worse absolute constant. The public Lean proof below carries this reduction out, with the constant $324K^2$ for every real set of at least five elements. The paper's Corollary 2.2, the sum-product exponent $\max(\lvert A+A\rvert,\lvert AA\rvert)\gg\lvert A\rvert^{4/3}/\log^{1/3}\lvert A\rvert$, is the result for which the paper is best known and is not the site's question. The statement is recorded from the card's reading of the paper, which records the read depth.

Depends on. Nothing in this wiki.

Acceptance. Refereed publication: Adv. Math. 222 (2009), no. 2, 402--408, doi:10.1016/j.aim.2009.04.006, in the October 2009 issue (Crossref record of 2026-10-07, which gives the issue month and no day). The preprint arXiv:0806.1040 was posted on 2008-06-05, the date of this page. Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits Solymosi [So09d] with the one-logarithm form of the bound (on 2026-10-07; the proof-claim tab is empty).

Formalization. Not counted as evidence: on 2026-04-25 Tomaz Mascarenhas posted to the site's thread that the prover Aristotle had autoformalized the solution from Solymosi's paper, with the explicit constant $324c$ for $\lvert A\rvert\ge5$, linking a Lean 4 file in a gist. The file, imported into Boris Alexeev's lean-proofs repository on 2026-05-07 (pinned above at the repository's commit of 2026-09-15; the file's header names Solymosi as informal author and Aristotle and Mascarenhas as formal authors), proves erdos_problem_818 for finite sets of positive reals with at least two elements,

$$\lvert A\rvert^2\le4c^2\lceil\log_2\lvert A\rvert\rceil\,\lvert AA\rvert \quad\text{when }\lvert A+A\rvert\le c\lvert A\rvert,$$

and erdos_problem_818_general for every finite set of reals with at least five elements, with the constant $324c^2$; its closing comment records #print axioms as propext, Classical.choice and Quot.sound, and the file contains no sorry. The formal-conjectures statement file, whose own theorem is sorry and whose statement ranges over finite sets of integers with a real exponent $C$ and the natural logarithm, names the repository's file on its main branch as the formal proof. The corpus holds no build of the development, so it gives no formalized evidence; no outside reviewer of the formal statement's fidelity to the site's question is recorded; and the community database on 2026-10-07 records the problem as "proved (Lean)" since 2026-04-25. The problem's standing rests on the refereed paper.