---

Claim. The answer to Problem 53 is yes: for every $k$, a finite set $A$ of integers with $\lvert A\rvert$ large in terms of $k$ has at least $\lvert A\rvert^k$ distinct integers that are a sum or a product of distinct elements of $A$. The claimed result is Theorem 2 of M.-C. Chang, The Erdős–Szemerédi problem on sum set and product set: with $A[1]$ the simple sums $\sum\varepsilon_ia_i$ and $A\{1\}$ the simple products $\prod a_i^{\varepsilon_i}$ ($\varepsilon_i\in\{0,1\}$) and $g(k)=\min_{\lvert A\rvert=k}(\lvert A[1]\rvert+\lvert A\{1\}\rvert)$, the theorem as printed says that there is $\varepsilon>0$ such that

$$k^{(\frac18-\varepsilon)\frac{\log k}{\log\log k}} <g(k)< k^{(1+\varepsilon)\frac{\log k}{\log\log k}}$$

(the paper's (0.21), with Remark 2.1 crediting Ruzsa with an improvement of $\frac18$ to $\frac12$). The form the deduction below needs is the one Section 2 proves, display (2.2): for every $\varepsilon>0$ and every $A\subset\mathbb N$ with $\lvert A\rvert=k$ large, $g(A)>k^{(\frac18-\varepsilon)\log k/\log\log k}$. With $\varepsilon<\frac18$ the lower exponent tends to infinity, so $g(k)$ exceeds $2k^m$ for every fixed $m$ once $k$ is large, and the union $A[1]\cup A\{1\}$, of size at least $g(k)/2$, exceeds $k^m$; this is the site's question. The paper poses the problem over sets of integers and proves the lower bound in its Section 2 for sets of positive integers, as Erdős and Szemerédi stated it; a set of $k$ integers has at least $(k-1)/2$ nonzero elements of one sign, and negating them preserves the number of distinct simple sums and the absolute values of the simple products, so the number of distinct products changes by at most a factor of two and the positive case still gives the general one with $k$ replaced by $(k-1)/2$, the sign-selection reduction recorded on the Erdős–Szemerédi card. The upper bound repeats the Erdős–Szemerédi construction (Section 3, Proposition 15) and shows $g(k)=k^{O(\log k/\log\log k)}$, so the growth is not exponential; with the lower bound, $g(k)$ is quasi-polynomial, faster than every fixed power of $k$ but slower than any exponential. The statement is as in the author's preprint, recorded on the source card; the proof is not checked in this corpus.

Depends on. Nothing in this wiki.

Acceptance. Reviewed: the site's curator, Thomas F. Bloom, labels the problem proved and credits Chang [Ch03] on the problem page with the solution in this form; the proof-claim tab was empty on 2026-10-07. Refereed publication: Ann. of Math. (2) 157 (2003), no. 3, 939--957, doi:10.4007/annals.2003.157.939, issued 1 May 2003 (Crossref record; the issue date names this page); the paper thanks the referee in its acknowledgement. The statement is cited from the author's preprint, not the journal version.

Formalization. The file src/latest/ErdosProblems/Erdos53.lean of Boris Alexeev's lean-proofs repository (first added 2026-08-17, pinned above at the commit of 2026-09-15) declares itself a formalization of this result: its header lists Erdős, Szemerédi and Chang as informal authors, Codex and GPT-5.6 Sol as formal authors, and Chang's paper as a primary reference. It proves Erdos53.erdos_53: for every k : ℕ there is N such that every A : Finset ℤ with at least N elements has A.card ^ k ≤ (sumProdValues A).card, where sumProdValues A is the union of Mathlib's A.subsetSum with the products over subsets of A. This is the right-hand side of the formal-conjectures statement for the problem without its answer(True) ↔ wrapper, except that the file's union counts the empty subset (the values $0$ and $1$) while the formal-conjectures sumsAndProducts erases it, a difference of at most two elements; the formal-conjectures statement file (revision of 2026-10-06) is tagged solved and names line 3084 of this file, the theorem, in its formal_proof attribute. The proof treats sets of positive integers through additive energy, Plünnecke–Ruzsa inequalities and a high-rank block argument, then passes to integer sets; it closes with #print axioms erdos_53 without the printed output. The community database (teorth/erdosproblems, file commit of 2026-09-28) lists the problem as "proved (Lean)" as of its last update of 2026-08-24 and formalized "yes" as of its last update of 2026-09-22. Neither record is an independent review of the whole statement, and this corpus has not built or audited the development, so the page lists no formalized evidence.