Wiki
Wiki

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

Updated

Problem 37

../

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


Statement. We say that A⊂NA\subset \mathbb{N} is an essential component if ds(A+B)>ds(B)d_s(A+B)>d_s(B) for every B⊂NB\subset \mathbb{N} with 0<ds(B)<10<d_s(B)<1 where dsd_s is the Schnirelmann density.

Can a lacunary set A⊂NA\subset\mathbb{N} be an essential component?

Status. DISPROVED (LEAN), the site's label; its suffix is a catalog label explained under Formalization. The status-defining source is Ruzsa's theorem (Proc. London Math. Soc. (3) 54 (1987), 38--56, refereed): an essential component AA satisfies ∣A∩{1,…,N}∣≥(log⁡N)1+c\lvert A\cap\{1,\ldots,N\}\rvert\ge(\log N)^{1+c} for some c>0c>0 and all large NN, while a lacunary set has only O(log⁡N)O(\log N) elements up to NN, so the answer is no. The claim page is Ruzsa, accepted on the site curator's credit and the refereed publication; the 2026 Lean development that declares itself a formalization of his theorem is linked there and gives no formalized evidence, since this corpus has not built or audited it.

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

References.

  • [Ru87] Ruzsa, I., Essential Components. Proc. London Math. Soc. (3) 54 (1987), no. 1, 38-56, doi:10.1112/plms/s3-54.1.38; not held.

Formalization. The Lean qualification in the site's label is a catalog label. formal-conjectures has no file for Problem 37, and the site's indicator reads "Formalised statement? No" (2026-10-07). The community database (teorth/erdosproblems, file commit of 2026-09-28) lists status "disproved (Lean)", 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. The locatable artifact is the Lean development src/latest/ErdosProblems/Erdos37.lean of Boris Alexeev's lean-proofs repository (added 2026-08-17; pinned on the Ruzsa claim page as a formalization of his theorem), which states the question under its own definitions. 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.