Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 53

claims/: The 1 claim page of Problem 53, one per claimant's result; the problem's standing derives from them.

Statement. Let $A$ be a finite set of integers. Is it true that, for every $k$ , if $\lvert A\rvert$ is sufficiently large depending on $k$ , then there are least $\lvert A\rvert^k$ many integers which are either the sum or product of distinct elements of $A$ ?

Status. PROVED (LEAN), the site's label; its suffix is a catalog label explained under Formalization. The status-defining source is Chang (Ann. of Math. (2) 157 (2003), 939--957, refereed). Section 2 proves the lower bound of her Theorem 2 in the form (2.2): $g(A)>k^{(\frac18-\varepsilon)\log k/\log\log k}$ for every $\varepsilon>0$ and every set $A$ of $k$ positive integers with $k$ large, where $g(A)$ is the number of simple sums plus the number of simple products of $A$ . Theorem 2 as printed, display (0.21), asserts its two bounds for some $\varepsilon>0$ . This bound exceeds every fixed power of $k$ ; the case of a set of integers of either sign follows by the sign reduction on the claim page, so the answer is yes. The claim page is Chang, accepted on the site curator's credit and the refereed publication; the 2026 Lean development that declares itself a formalization of her result is linked there and gives no formalized evidence, since this corpus has not built or audited it.

Source. erdosproblems.com/53, accessed 2026-09-04 and 2026-10-07 (no last-edited date shown; empty proof-claim tab). Cite as: T. F. Bloom, Erdős Problem #53, https://www.erdosproblems.com/53.

References.

[Ch03] Chang, M.-C., The Erdős-Szemerédi problem on sum set and product set. Ann. of Math. (2) 157 (2003), no. 3, 939-957, doi:10.4007/annals.2003.157.939 (Crossref record, 2026-10-07); cited from the author's preprint. Library home: chang_2003_erdos_szemeredi_problem_sum_set_product_set.
[ErSz83] Erdős, P. and Szemerédi, E., On sums and products of integers. Studies in pure mathematics (1983), 213-218.

Formalization. The Lean qualification in the site's label is a catalog label. The statement is in formal-conjectures, over Finset ℤ; at its commit of 2026-10-06, the one linked, the file is tagged solved and names line 3084 of src/latest/ErdosProblems/Erdos53.lean of Boris Alexeev's lean-proofs repository as the formal proof. The community database (teorth/erdosproblems, file commit of 2026-09-28) lists the status "proved (Lean)" as of its last update of 2026-08-24 and formalized "yes" as of its last update of 2026-09-22. The development (added 2026-08-17) is pinned on the Chang claim page as a formalization of her result. This corpus has not built or checked it, and no local kernel credit is claimed.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (7)

Chang proves the simple sums and products exceed every power problems/additive_combinatorics/E0053/claims Sumsets and Arithmetic Progressions additive_combinatorics/chang_2003_erdos_szemeredi_problem_sum_set_product_set Theorem 2 (p. 4): the least number g(k) of simple sums plus simple products of k positive integers satisfies log g(k) ≍ (log k)^2/log log k additive_combinatorics/erdos_1983_sums_products_integers Theorem 2 (p. 214): g(n) < exp(c_3 log^2 n / log log n) for the least number of subset sums and subset products of n positive integers

Graph