---

Claim. The answer to Problem 37 is no: a lacunary set is never an essential component. The claimed result is the main theorem of I. Z. Ruzsa, Essential components: if $A\subset\mathbb N$ is an essential component, so that $d_s(A+B)>d_s(B)$ for every $B$ with $0<d_s(B)<1$, then there is a constant $c>0$ with

$$\lvert A\cap\{1,\ldots,N\}\rvert\ge(\log N)^{1+c}$$

for all large $N$. A lacunary set, whose consecutive elements grow by at least a fixed ratio $q>1$ ($a_{i+1}\ge q\,a_i$), has at most $\log N/\log q+O(1)$ elements up to $N$, so it fails this bound and cannot be an essential component. Ruzsa also shows the exponent is sharp: for every $c>0$ there is an essential component with at most $(\log N)^{1+c}$ elements up to $N$ for all large $N$. The theorem is stated here in the form the site's commentary gives it; the paper is not held in the library, and its 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 disproved and credits the resolution to Ruzsa [Ru87] on the problem page; the proof-claim tab was empty on 2026-10-07. Refereed publication: Proc. London Math. Soc. (3) 54 (1987), no. 1, 38--56, doi:10.1112/plms/s3-54.1.38; the Crossref record dates the print issue to January 1987, filled to the first of the month for this page's name, and gives the online date 2016-12-23. The Plünnecke bound compiled on the Jin card shows that every Schnirelmann basis is an essential component; it is background on the notion and bears neither way on lacunary sets.

Formalization. The file src/latest/ErdosProblems/Erdos37.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 theorem: its header lists Ruzsa as informal author and Codex and GPT-5.6 Sol as formal authors. It proves Erdos37.not_erdos_37, that every A : Set ℕ satisfying IsLacunary A fails IsEssentialComponent A, under its own definitions, since formal-conjectures has no statement for the problem: sd is Mathlib's schnirelmannDensity; IsEssentialComponent A says that $d_s(B)<d_s(A+B)$ for every $B$ with $0<d_s(B)<1$, with pointwise addition of sets of nonnegative integers; and IsLacunary A says that the positive part of $A$ is infinite and that consecutive members of its increasing enumeration grow by at least a fixed real ratio $q>1$ ($q\,a_i\le a_{i+1}$). The proof constructs, from lacunarity and $0\in A$, a set $C$ of Schnirelmann density $\delta\in(0,1)$ with $d_s(A+C)=d_s(C)$, which contradicts the essential-component property; it closes with #print axioms not_erdos_37 without the printed output. The community database (teorth/erdosproblems, file commit of 2026-09-28) lists the problem as "disproved (Lean)", with formal_status Lean and formalized "no", as of its last update on 2026-08-24, without recording when that state was set, and names no artifact. This corpus has not built or audited the development, and the fidelity of its definitions to the site's question has not been independently reviewed, so the page lists no formalized evidence.